112 resulting rule, for later use with the 'cases' method (cf. attribute |
112 resulting rule, for later use with the 'cases' method (cf. attribute |
113 case_names). |
113 case_names). |
114 |
114 |
115 * Isar: 'obtain' takes an optional case name for the local context |
115 * Isar: 'obtain' takes an optional case name for the local context |
116 introduction rule (default "that"). |
116 introduction rule (default "that"). |
|
117 |
|
118 * Isar/locales: new derived specification elements 'definition', |
|
119 'abbreviation', 'axiomatization', which support type-inference, admit |
|
120 object-level specifications (equality, equivalence), and may used |
|
121 within an optional locale context. For example: |
|
122 |
|
123 definition |
|
124 "f x y = x + y + 1" |
|
125 "g x = f x x" |
|
126 |
|
127 thm f_def g_def |
|
128 |
|
129 axiomatization |
|
130 eq (infix "===" 50) |
|
131 where eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y" |
|
132 |
|
133 abbreviation (output) |
|
134 neq (infix "=!=" 50) |
|
135 "(x =!= y) <-> ~ (x === y)" |
|
136 |
|
137 Within a locale context, constants being introduced depend on certain |
|
138 fixed parameters, and the constant name is qualified by the locale |
|
139 base name. An internal abbreviation takes care for convenient input |
|
140 and output, making the parameters implicit and using the original |
|
141 short name. Presently, abbreviations are only available "in" a target |
|
142 locale, but not inherited by general import expressions. |
|
143 |
|
144 See the isar-ref manual for further details. |
117 |
145 |
118 * Provers/induct: improved internal context management to support |
146 * Provers/induct: improved internal context management to support |
119 local fixes and defines on-the-fly. Thus explicit meta-level |
147 local fixes and defines on-the-fly. Thus explicit meta-level |
120 connectives !! and ==> are rarely required anymore in inductive goals |
148 connectives !! and ==> are rarely required anymore in inductive goals |
121 (using object-logic connectives for this purpose has been long |
149 (using object-logic connectives for this purpose has been long |
361 mangling (bijective mapping from any expression values to strings). |
389 mangling (bijective mapping from any expression values to strings). |
362 |
390 |
363 * Pure/General/rat.ML implements rational numbers. |
391 * Pure/General/rat.ML implements rational numbers. |
364 |
392 |
365 * Pure/General/table.ML: the join operations now works via exceptions |
393 * Pure/General/table.ML: the join operations now works via exceptions |
366 DUP/SAME instead of type option. This is both simpler and admits |
394 DUP/SAME instead of type option. This is simpler in simple cases, and |
367 slightly more efficient complex applications. |
395 admits slightly more efficient complex applications. |
368 |
396 |
369 * Pure: datatype Context.generic joins theory/Proof.context and |
397 * Pure: datatype Context.generic joins theory/Proof.context and |
370 provides some facilities for code that works in either kind of |
398 provides some facilities for code that works in either kind of |
371 context, notably GenericDataFun for uniform theory and proof data. |
399 context, notably GenericDataFun for uniform theory and proof data. |
372 |
400 |