# HG changeset patch
# User nipkow
# Date 1183551001 -7200
# Node ID ae0e735fbec8e868609a72f4ac81b15ee636a146
# Parent  42f2f90b51a645abf3ba3c9ee0426b8bc4313a7b
*** empty log message ***

diff -r 42f2f90b51a6 -r ae0e735fbec8 NEWS
--- 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"