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 nonlogical types should be declared as 'nonterminals' 
154 Note that nonlogical types should be declared as 'nonterminals' 
155 rather than 'types'. INCOMPATIBILITY for new objectlogic 
155 rather than 'types'. INCOMPATIBILITY for new objectlogic 
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 *** 