equal
deleted
inserted
replaced
37 process, without requiring oldfashioned commandline invocation of 
37 process, without requiring oldfashioned commandline invocation of 
38 "isabelle jedit m MODE". 
38 "isabelle jedit m MODE". 
39 
39 
40 
40 
41 *** Pure *** 
41 *** Pure *** 

42 

43 * Attributes "where" and "of" allow an optional context of local 

44 variables ('for' declaration): these variables become schematic in the 

45 instantiated theorem. 
42 
46 
43 * More thorough check of proof context for goal statements and 
47 * More thorough check of proof context for goal statements and 
44 attributed fact expressions (concerning background theory, declared 
48 attributed fact expressions (concerning background theory, declared 
45 hyps). Potential INCOMPATIBILITY, tools need to observe standard 
49 hyps). Potential INCOMPATIBILITY, tools need to observe standard 
46 context discipline. See also Assumption.add_assumes and the more 
50 context discipline. See also Assumption.add_assumes and the more 
266 explicit setcomprehensions with eucl_less for other (half) open 
270 explicit setcomprehensions with eucl_less for other (half) open 
267 intervals. 
271 intervals. 
268 
272 
269 
273 
270 *** ML *** 
274 *** ML *** 

275 

276 * Proper context discipline for read_instantiate and instantiate_tac: 

277 variables that are meant to become schematic need to be given as 

278 fixed, and are generalized by the explicit context of local variables. 

279 This corresponds to Isar attributes "where" and "of" with 'for' 

280 declaration. INCOMPATIBILITY, also due to potential change of indices 

281 of schematic variables. 
271 
282 
272 * Toplevel function "use" refers to raw ML bootstrap environment, 
283 * Toplevel function "use" refers to raw ML bootstrap environment, 
273 without Isar context nor antiquotations. Potential INCOMPATIBILITY. 
284 without Isar context nor antiquotations. Potential INCOMPATIBILITY. 
274 Note that 'ML_file' is the canonical command to load ML files into the 
285 Note that 'ML_file' is the canonical command to load ML files into the 
275 formal context. 
286 formal context. 