[isabelle-dev] NEWS: case/lambda syntax
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