[isabelle-dev] NEWS: case/lambda syntax

Tobias Nipkow nipkow at in.tum.de
Wed Jul 4 14:14:48 CEST 2007

* Case-expressions allow arbitrary constructor-patterns (including "_") and
   takes their order into account, like in functional programming.
   Internally, this is translated into nested case-expressions; missing 
   are added and mapped to the predefined constant "undefined". In 
   cases printing may no longer show the original input but the internal
   form. Lambda-abstraction allows the same form of pattern matching:
   "% pat1 => e1 | ..." is an abbreviation for
   "%x. case x of pat1 => e1 | ..." where x is a new variable.

More information about the isabelle-dev mailing list