> I assume, `% pat1 => e1 | pat2 => e2' is equivalent to > > % a0 . case a0 of pat1 => e1 | pat2 => e2 > > with `a0' being a fresh identifier. Yes. > How does a multiple-arguments (automatically curried) lambda look like? It doesn't exist. At least not in Isabelle. BTW, list comprehension is input syntax only at the moment. Tobias