equal
deleted
inserted
replaced
78 
78 
79 better use "obtain" in situations as above; alternative refer to 
79 better use "obtain" in situations as above; alternative refer to 
80 multistep methods like 'auto', 'simp_all', 'blast+' etc.; 
80 multistep methods like 'auto', 'simp_all', 'blast+' etc.; 
81 
81 
82 * Pure: proper integration with ``locales''; unlike the original 
82 * Pure: proper integration with ``locales''; unlike the original 
83 version by Florian Kammueller, Isar locales package highlevel proof 
83 version by Florian Kammüller, Isar locales package highlevel proof 
84 contexts rather than raw logical ones (e.g. we admit to include 
84 contexts rather than raw logical ones (e.g. we admit to include 
85 attributes everywhere); 
85 attributes everywhere); 
86 
86 
87 * Pure: theory goals now support adhoc contexts, which are discharged 
87 * Pure: theory goals now support adhoc contexts, which are discharged 
88 in the result, as in ``lemma (assumes A and B) K: A .''; syntax 
88 in the result, as in ``lemma (assumes A and B) K: A .''; syntax 
189 
189 
190 * HOL: syntax translations now work properly with numerals and records 
190 * HOL: syntax translations now work properly with numerals and records 
191 expressions; 
191 expressions; 
192 
192 
193 * HOL/GroupTheory: group theory examples including Sylow's theorem, by 
193 * HOL/GroupTheory: group theory examples including Sylow's theorem, by 
194 Florian Kammüller; 
194 Florian Kammüller; 
195 
195 
196 * HOL: got rid of some global declarations (potential INCOMPATIBILITY 
196 * HOL: got rid of some global declarations (potential INCOMPATIBILITY 
197 for ML tools): const "()" renamed "Product_Type.Unity", type "unit" 
197 for ML tools): const "()" renamed "Product_Type.Unity", type "unit" 
198 renamed "Product_Type.unit"; 
198 renamed "Product_Type.unit"; 
199 
199 
207 HOLCF/ex/Dnat.thy; 
207 HOLCF/ex/Dnat.thy; 
208 
208 
209 
209 
210 *** ZF *** 
210 *** ZF *** 
211 
211 
212 * ZF: newstyle theory commands 'inductive', 'inductive_cases', and 
212 * ZF: newstyle theory commands '(co)inductive', '(co)datatype', 
213 methods 'ind_cases', 'induct_tac', 'case_tac'; 
213 'rep_datatype', 'inductive_cases'; also methods 'ind_cases', 

214 'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC'); 
214 
215 
215 * ZF: the integer library now covers quotients and remainders, with 
216 * ZF: the integer library now covers quotients and remainders, with 
216 many laws relating division to addition, multiplication, etc.; 
217 many laws relating division to addition, multiplication, etc.; 
217 
218 
218 * ZF/Induct: new directory for examples of inductive definitions, 
219 * ZF/Induct: new directory for examples of inductive definitions, 