equal
deleted
inserted
replaced
12 |
12 |
13 * Theory syntax: the old non-Isar theory file format has been |
13 * Theory syntax: the old non-Isar theory file format has been |
14 discontinued altogether. Note that ML proof scripts may still be used |
14 discontinued altogether. Note that ML proof scripts may still be used |
15 with Isar theories; migration is usually quite simple with the ML |
15 with Isar theories; migration is usually quite simple with the ML |
16 function use_legacy_bindings. INCOMPATIBILITY. |
16 function use_legacy_bindings. INCOMPATIBILITY. |
|
17 |
|
18 * Theory syntax: some popular names (e.g. "class", "if") are now |
|
19 keywords. INCOMPATIBILITY, use double quotes. |
17 |
20 |
18 * Legacy goal package: reduced interface to the bare minimum required |
21 * Legacy goal package: reduced interface to the bare minimum required |
19 to keep existing proof scripts running. Most other user-level |
22 to keep existing proof scripts running. Most other user-level |
20 functions are now part of the OldGoals structure, which is *not* open |
23 functions are now part of the OldGoals structure, which is *not* open |
21 by default (consider isatool expandshort before open OldGoals). |
24 by default (consider isatool expandshort before open OldGoals). |
101 method expression within a sandbox consisting of the first N |
104 method expression within a sandbox consisting of the first N |
102 sub-goals, which need to exist. For example, ``simp_all [3]'' |
105 sub-goals, which need to exist. For example, ``simp_all [3]'' |
103 simplifies the first three sub-goals, while (rule foo, simp_all)[] |
106 simplifies the first three sub-goals, while (rule foo, simp_all)[] |
104 simplifies all new goals that emerge from applying rule foo to the |
107 simplifies all new goals that emerge from applying rule foo to the |
105 originally first one. |
108 originally first one. |
|
109 |
|
110 * Isar: schematic goals are no longer restricted to higher-order |
|
111 patterns; e.g. ``lemma "?P(?x)" by (rule TrueI)'' now works as |
|
112 expected. |
106 |
113 |
107 * Isar: the conclusion of a long theorem statement is now either |
114 * Isar: the conclusion of a long theorem statement is now either |
108 'shows' (a simultaneous conjunction, as before), or 'obtains' |
115 'shows' (a simultaneous conjunction, as before), or 'obtains' |
109 (essentially a disjunction of cases with local parameters and |
116 (essentially a disjunction of cases with local parameters and |
110 assumptions). The latter allows to express general elimination rules |
117 assumptions). The latter allows to express general elimination rules |
521 declarations and definitions. |
528 declarations and definitions. |
522 |
529 |
523 * Pure/kernel: consts certification ignores sort constraints given in |
530 * Pure/kernel: consts certification ignores sort constraints given in |
524 signature declarations. (This information is not relevant to the |
531 signature declarations. (This information is not relevant to the |
525 logic, but only for type inference.) IMPORTANT INTERNAL CHANGE. |
532 logic, but only for type inference.) IMPORTANT INTERNAL CHANGE. |
|
533 |
|
534 * Pure: Logic.(un)varify only works in a global context, which is now |
|
535 enforced instead of silently assumed. INCOMPATIBILITY, may use |
|
536 Logic.legacy_(un)varify as temporary workaround. |
526 |
537 |
527 * Pure: axiomatic type classes are now purely definitional, with |
538 * Pure: axiomatic type classes are now purely definitional, with |
528 explicit proofs of class axioms and super class relations performed |
539 explicit proofs of class axioms and super class relations performed |
529 internally. See Pure/axclass.ML for the main internal interfaces -- |
540 internally. See Pure/axclass.ML for the main internal interfaces -- |
530 notably AxClass.define_class supercedes AxClass.add_axclass, and |
541 notably AxClass.define_class supercedes AxClass.add_axclass, and |