153 * Removed obsolete type class "logic", use the top sort {} instead. |
153 * Removed obsolete type class "logic", use the top sort {} instead. |
154 Note that non-logical types should be declared as 'nonterminals' |
154 Note that non-logical types should be declared as 'nonterminals' |
155 rather than 'types'. INCOMPATIBILITY for new object-logic |
155 rather than 'types'. INCOMPATIBILITY for new object-logic |
156 specifications. |
156 specifications. |
157 |
157 |
|
158 * Attributes 'induct' and 'cases': type or set names may now be |
|
159 locally fixed variables as well. |
|
160 |
158 * Simplifier: can now control the depth to which conditional rewriting |
161 * Simplifier: can now control the depth to which conditional rewriting |
159 is traced via the PG menu Isabelle -> Settings -> Trace Simp Depth |
162 is traced via the PG menu Isabelle -> Settings -> Trace Simp Depth |
160 Limit. |
163 Limit. |
161 |
164 |
162 * Simplifier: simplification procedures may now take the current |
165 * Simplifier: simplification procedures may now take the current |
184 * More efficient treatment of intermediate checkpoints in interactive |
187 * More efficient treatment of intermediate checkpoints in interactive |
185 theory development. |
188 theory development. |
186 |
189 |
187 |
190 |
188 *** Locales *** |
191 *** Locales *** |
189 |
192 |
190 * New commands for the interpretation of locale expressions in |
193 * New commands for the interpretation of locale expressions in theories (1), |
191 theories ('interpretation') and proof contexts ('interpret'). These |
194 locales (2) and proof contexts (3). These generate proof obligations from |
192 take an instantiation of the locale parameters and compute proof |
195 the expression specification. After the obligations have been discharged, |
193 obligations from the instantiated specification. After the |
196 theorems of the expression are added to the theory, target locale or proof |
194 obligations have been discharged, the instantiated theorems of the |
197 context. The synopsis of the commands is a follows: |
195 locale are added to the theory or proof context. Interpretation is |
198 (1) interpretation expr inst |
196 smart in that already active interpretations do not occur in proof |
199 (2) interpretation target < expr |
197 obligations, neither are instantiated theorems stored in duplicate. |
200 (3) interpret expr inst |
198 Use print_interps to inspect active interpretations of a particular |
201 Interpretation in theories and proof contexts require a parameter |
199 locale. For details, see the Isar Reference manual. |
202 instantiation of terms from the current context. This is applied to |
|
203 specifications and theorems of the interpreted expression. Interpretation |
|
204 in locales only permits parameter renaming through the locale expression. |
|
205 Interpretation is smart in that interpretation that are active already |
|
206 do not occur in proof obligations, neither are instantiated theorems stored |
|
207 in duplicate. Use 'print_interps' to inspect active interpretations of |
|
208 a particular locale. For details, see the Isar Reference manual. |
200 |
209 |
201 INCOMPATIBILITY: former 'instantiate' has been withdrawn, use |
210 INCOMPATIBILITY: former 'instantiate' has been withdrawn, use |
202 'interpret' instead. |
211 'interpret' instead. |
|
212 |
|
213 * New context element 'constrains' for adding type constraints to parameters. |
|
214 |
|
215 * Context expressions: renaming of parameters with syntax redeclaration. |
|
216 |
|
217 * Locale declaration: 'includes' disallowed. |
203 |
218 |
204 * Proper static binding of attribute syntax -- i.e. types / terms / |
219 * Proper static binding of attribute syntax -- i.e. types / terms / |
205 facts mentioned as arguments are always those of the locale definition |
220 facts mentioned as arguments are always those of the locale definition |
206 context, independently of the context of later invocations. Moreover, |
221 context, independently of the context of later invocations. Moreover, |
207 locale operations (renaming and type / term instantiation) are applied |
222 locale operations (renaming and type / term instantiation) are applied |
216 intervention. Only unusual applications -- such as "where" or "of" |
231 intervention. Only unusual applications -- such as "where" or "of" |
217 (cf. src/Pure/Isar/attrib.ML), which process arguments depending both |
232 (cf. src/Pure/Isar/attrib.ML), which process arguments depending both |
218 on the context and the facts involved -- may have to assign parsed |
233 on the context and the facts involved -- may have to assign parsed |
219 values to argument tokens explicitly. |
234 values to argument tokens explicitly. |
220 |
235 |
221 * New context element "constrains" adds type constraints to parameters -- |
|
222 there is no logical significance. |
|
223 |
|
224 * Context expressions: renaming parameters permits syntax |
|
225 redeclaration as well. |
|
226 |
|
227 * Locale definition: 'includes' now disallowed. |
|
228 |
|
229 * Changed parameter management in theorem generation for long goal |
236 * Changed parameter management in theorem generation for long goal |
230 statements with 'includes'. INCOMPATIBILITY: produces a different |
237 statements with 'includes'. INCOMPATIBILITY: produces a different |
231 theorem statement in rare situations. |
238 theorem statement in rare situations. |
232 |
239 |
233 * Attributes 'induct' and 'cases': type or set names may now be |
240 * Antiquotations provide the option 'locale=NAME' to specify an |
234 locally fixed variables as well. |
|
235 |
|
236 * Antiquotations now provide the option 'locale=NAME' to specify an |
|
237 alternative context used for evaluating and printing the subsequent |
241 alternative context used for evaluating and printing the subsequent |
238 argument, as in @{thm [locale=LC] fold_commute}, for example. |
242 argument, as in @{thm [locale=LC] fold_commute}, for example. |
239 |
243 |
240 |
244 |
241 *** Provers *** |
245 *** Provers *** |