* HOL finally supports full list comprehensions as in Haskell, except that "." is used instead of "|". As a by-product, pattern-matching abstractions "% pat1 => e1 | ..." are supported as well.