equal
deleted
inserted
replaced
126 proof context in long statement form, according to the syntax of a |
126 proof context in long statement form, according to the syntax of a |
127 top-level lemma. |
127 top-level lemma. |
128 |
128 |
129 * Isar: 'obtain' takes an optional case name for the local context |
129 * Isar: 'obtain' takes an optional case name for the local context |
130 introduction rule (default "that"). |
130 introduction rule (default "that"). |
|
131 |
|
132 * Isar: removed obsolete 'concl is' patterns. INCOMPATIBILITY, use |
|
133 explicit (is "_ ==> ?foo") in the rare cases where this still happens |
|
134 to occur. |
131 |
135 |
132 * Isar/locales: new derived specification elements 'definition', |
136 * Isar/locales: new derived specification elements 'definition', |
133 'abbreviation', 'axiomatization', which support type-inference, admit |
137 'abbreviation', 'axiomatization', which support type-inference, admit |
134 object-level specifications (equality, equivalence). See also the |
138 object-level specifications (equality, equivalence). See also the |
135 isar-ref manual. Examples: |
139 isar-ref manual. Examples: |