equal
deleted
inserted
replaced
40 * Discontinued empty name bindings in 'axiomatization'. |
40 * Discontinued empty name bindings in 'axiomatization'. |
41 INCOMPATIBILITY. |
41 INCOMPATIBILITY. |
42 |
42 |
43 |
43 |
44 *** HOL *** |
44 *** HOL *** |
|
45 |
|
46 * Nested case expressions are now translated in a separate check |
|
47 phase rather than during parsing. The data for case combinators |
|
48 is separated from the datatype package. The declaration attribute |
|
49 "case_translation" can be used to register new case combinators: |
|
50 |
|
51 declare [[case_translation case_combinator constructor1 ... constructorN]] |
45 |
52 |
46 * Notation "{p:A. P}" now allows tuple patterns as well. |
53 * Notation "{p:A. P}" now allows tuple patterns as well. |
47 |
54 |
48 * Revised devices for recursive definitions over finite sets: |
55 * Revised devices for recursive definitions over finite sets: |
49 - Only one fundamental fold combinator on finite set remains: |
56 - Only one fundamental fold combinator on finite set remains: |