*** empty log message ***
authornipkow
Wed Jul 04 14:10:01 2007 +0200 (2007-07-04)
changeset 23564ae0e735fbec8
parent 23563 42f2f90b51a6
child 23565 c00b12a4e245
*** empty log message ***
NEWS
     1.1 --- a/NEWS	Wed Jul 04 13:56:26 2007 +0200
     1.2 +++ b/NEWS	Wed Jul 04 14:10:01 2007 +0200
     1.3 @@ -550,6 +550,15 @@
     1.4  successful. These can be pasted into the proof.  Users do not have to
     1.5  wait for the automatic provers to return.
     1.6  
     1.7 +* Case-expressions allow arbitrary constructor-patterns (including "_") and
     1.8 +  takes their order into account, like in functional programming.
     1.9 +  Internally, this is translated into nested case-expressions; missing cases
    1.10 +  are added and mapped to the predefined constant "undefined". In complicated
    1.11 +  cases printing may no longer show the original input but the internal
    1.12 +  form. Lambda-abstraction allows the same form of pattern matching:
    1.13 +  "% pat1 => e1 | ..." is an abbreviation for
    1.14 +  "%x. case x of pat1 => e1 | ..." where x is a new variable.
    1.15 +
    1.16  * IntDef: The constant "int :: nat => int" has been removed; now "int"
    1.17    is an abbreviation for "of_nat :: nat => int". The simplification rules
    1.18    for "of_nat" have been changed to work like "int" did previously.
    1.19 @@ -587,8 +596,7 @@
    1.20      Orderings.max ~> Orderings.ord_class.max
    1.21      FixedPoint.Sup ~> FixedPoint.complete_lattice_class.Sup
    1.22  
    1.23 -* case expressions and primrec: missing cases now mapped to "undefined"
    1.24 -instead of "arbitrary"
    1.25 +* primrec: missing cases mapped to "undefined" instead of "arbitrary"
    1.26  
    1.27  * new constant "undefined" with axiom "undefined x = undefined"
    1.28