--- a/NEWS Wed Jul 04 13:56:26 2007 +0200
+++ b/NEWS Wed Jul 04 14:10:01 2007 +0200
@@ -550,6 +550,15 @@
successful. These can be pasted into the proof. Users do not have to
wait for the automatic provers to return.
+* 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 cases
+ are added and mapped to the predefined constant "undefined". In complicated
+ 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.
+
* IntDef: The constant "int :: nat => int" has been removed; now "int"
is an abbreviation for "of_nat :: nat => int". The simplification rules
for "of_nat" have been changed to work like "int" did previously.
@@ -587,8 +596,7 @@
Orderings.max ~> Orderings.ord_class.max
FixedPoint.Sup ~> FixedPoint.complete_lattice_class.Sup
-* case expressions and primrec: missing cases now mapped to "undefined"
-instead of "arbitrary"
+* primrec: missing cases mapped to "undefined" instead of "arbitrary"
* new constant "undefined" with axiom "undefined x = undefined"