39 
39 
40 prints the last 100 theorems matching the pattern "(_::nat) + _ + _", 
40 prints the last 100 theorems matching the pattern "(_::nat) + _ + _", 
41 matching the current goal as introduction rule and not having "HOL." 
41 matching the current goal as introduction rule and not having "HOL." 
42 in their name (i.e. not being defined in theory HOL). 
42 in their name (i.e. not being defined in theory HOL). 
43 
43 

44 * Communication with Proof General is now 8bit clean, which means that 

45 Unicode text in UTF8 encoding may be used within theory texts (both 

46 formal and informal parts). See option U of the Isabelle Proof 

47 General interface. 

48 
44 
49 
45 *** Document preparation *** 
50 *** Document preparation *** 
46 
51 
47 * Commands 'display_drafts' and 'print_drafts' perform simple output 
52 * Commands 'display_drafts' and 'print_drafts' perform simple output 
48 of raw sources. Only those symbols that do not require additional 
53 of raw sources. Only those symbols that do not require additional 
222 theory development. 
227 theory development. 
223 
228 
224 
229 
225 *** Locales *** 
230 *** Locales *** 
226 
231 
227 * New commands for the interpretation of locale expressions in theories (1), 
232 * New commands for the interpretation of locale expressions in 
228 locales (2) and proof contexts (3). These generate proof obligations from 
233 theories (1), locales (2) and proof contexts (3). These generate 
229 the expression specification. After the obligations have been discharged, 
234 proof obligations from the expression specification. After the 
230 theorems of the expression are added to the theory, target locale or proof 
235 obligations have been discharged, theorems of the expression are added 
231 context. The synopsis of the commands is a follows: 
236 to the theory, target locale or proof context. The synopsis of the 

237 commands is a follows: 

238 
232 (1) interpretation expr inst 
239 (1) interpretation expr inst 
233 (2) interpretation target < expr 
240 (2) interpretation target < expr 
234 (3) interpret expr inst 
241 (3) interpret expr inst 

242 
235 Interpretation in theories and proof contexts require a parameter 
243 Interpretation in theories and proof contexts require a parameter 
236 instantiation of terms from the current context. This is applied to 
244 instantiation of terms from the current context. This is applied to 
237 specifications and theorems of the interpreted expression. Interpretation 
245 specifications and theorems of the interpreted expression. 
238 in locales only permits parameter renaming through the locale expression. 
246 Interpretation in locales only permits parameter renaming through the 
239 Interpretation is smart in that interpretations that are active already 
247 locale expression. Interpretation is smart in that interpretations 
240 do not occur in proof obligations, neither are instantiated theorems stored 
248 that are active already do not occur in proof obligations, neither are 
241 in duplicate. Use 'print_interps' to inspect active interpretations of 
249 instantiated theorems stored in duplicate. Use 'print_interps' to 
242 a particular locale. For details, see the Isar Reference manual. 
250 inspect active interpretations of a particular locale. For details, 

251 see the Isar Reference manual. 
243 
252 
244 INCOMPATIBILITY: former 'instantiate' has been withdrawn, use 
253 INCOMPATIBILITY: former 'instantiate' has been withdrawn, use 
245 'interpret' instead. 
254 'interpret' instead. 
246 
255 
247 * New context element 'constrains' for adding type constraints to parameters. 
256 * New context element 'constrains' for adding type constraints to 
248 
257 parameters. 
249 * Context expressions: renaming of parameters with syntax redeclaration. 
258 

259 * Context expressions: renaming of parameters with syntax 

260 redeclaration. 
250 
261 
251 * Locale declaration: 'includes' disallowed. 
262 * Locale declaration: 'includes' disallowed. 
252 
263 
253 * Proper static binding of attribute syntax  i.e. types / terms / 
264 * Proper static binding of attribute syntax  i.e. types / terms / 
254 facts mentioned as arguments are always those of the locale definition 
265 facts mentioned as arguments are always those of the locale definition 