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 |
117 |
118 * Isar/locales: new derived specification elements 'definition', |
118 * Isar/locales: new derived specification elements 'definition', |
119 'abbreviation', 'axiomatization', which support type-inference, admit |
119 'abbreviation', 'axiomatization', which support type-inference, admit |
120 object-level specifications (equality, equivalence), and may used |
120 object-level specifications (equality, equivalence). See also the |
121 within an optional locale context. For example: |
121 isar-ref manual. Examples: |
122 |
122 |
123 definition |
123 definition |
124 "f x y = x + y + 1" |
124 "f x y = x + y + 1" |
125 "g x = f x x" |
125 "g x = f x x" |
126 |
126 |
132 |
132 |
133 abbreviation (output) |
133 abbreviation (output) |
134 neq (infix "=!=" 50) |
134 neq (infix "=!=" 50) |
135 "(x =!= y) <-> ~ (x === y)" |
135 "(x =!= y) <-> ~ (x === y)" |
136 |
136 |
137 Within a locale context, constants being introduced depend on certain |
137 These specifications may be also used in a locale context. Then the |
138 fixed parameters, and the constant name is qualified by the locale |
138 constants being introduced depend on certain fixed parameters, and the |
139 base name. An internal abbreviation takes care for convenient input |
139 constant name is qualified by the locale base name. An internal |
140 and output, making the parameters implicit and using the original |
140 abbreviation takes care for convenient input and output, making the |
141 short name. Presently, abbreviations are only available "in" a target |
141 parameters implicit and using the original short name. See |
142 locale, but not inherited by general import expressions. |
142 HOL/ex/Abstract_NAT.thy for an example of deriving polymorphic |
143 |
143 entities from a monomorphic theory. |
144 See the isar-ref manual for further details. |
144 |
|
145 Presently, abbreviations are only available 'in' a target locale, but |
|
146 not inherited by general import expressions. |
145 |
147 |
146 * Provers/induct: improved internal context management to support |
148 * Provers/induct: improved internal context management to support |
147 local fixes and defines on-the-fly. Thus explicit meta-level |
149 local fixes and defines on-the-fly. Thus explicit meta-level |
148 connectives !! and ==> are rarely required anymore in inductive goals |
150 connectives !! and ==> are rarely required anymore in inductive goals |
149 (using object-logic connectives for this purpose has been long |
151 (using object-logic connectives for this purpose has been long |