summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 23564 | ae0e735fbec8 |

parent 23562 | 6cad6b400cfd |

child 23565 | c00b12a4e245 |

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