142 |
142 |
143 axiomatization |
143 axiomatization |
144 eq (infix "===" 50) |
144 eq (infix "===" 50) |
145 where eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y" |
145 where eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y" |
146 |
146 |
147 abbreviation (output) |
147 abbreviation |
148 neq (infix "=!=" 50) |
148 neq (infix "=!=" 50) |
149 "(x =!= y) <-> ~ (x === y)" |
149 "x =!= y == ~ (x === y)" |
150 |
150 |
151 These specifications may be also used in a locale context. Then the |
151 These specifications may be also used in a locale context. Then the |
152 constants being introduced depend on certain fixed parameters, and the |
152 constants being introduced depend on certain fixed parameters, and the |
153 constant name is qualified by the locale base name. An internal |
153 constant name is qualified by the locale base name. An internal |
154 abbreviation takes care for convenient input and output, making the |
154 abbreviation takes care for convenient input and output, making the |
155 parameters implicit and using the original short name. See also |
155 parameters implicit and using the original short name. See also |
156 HOL/ex/Abstract_NAT.thy for an example of deriving polymorphic |
156 HOL/ex/Abstract_NAT.thy for an example of deriving polymorphic |
157 entities from a monomorphic theory. |
157 entities from a monomorphic theory. |
158 |
158 |
159 Presently, abbreviations are only available 'in' a target locale, but |
159 Presently, abbreviations are only available 'in' a target locale, but |
160 not inherited by general import expressions. |
160 not inherited by general import expressions. Also note that |
161 |
161 'abbreviation' may be used as a type-safe replacement for 'syntax' + |
162 Also note that 'abbreviation' may be used as a type-safe replacement |
162 'translations' in common applications. |
163 for 'syntax' + 'translations' in common applications. |
|
164 |
163 |
165 * Provers/induct: improved internal context management to support |
164 * Provers/induct: improved internal context management to support |
166 local fixes and defines on-the-fly. Thus explicit meta-level |
165 local fixes and defines on-the-fly. Thus explicit meta-level |
167 connectives !! and ==> are rarely required anymore in inductive goals |
166 connectives !! and ==> are rarely required anymore in inductive goals |
168 (using object-logic connectives for this purpose has been long |
167 (using object-logic connectives for this purpose has been long |