equal
deleted
inserted
replaced
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 

213 methods 'ind_cases', 'induct_tac', 'case_tac'; 

214 
212 * ZF: the integer library now covers quotients and remainders, with 
215 * ZF: the integer library now covers quotients and remainders, with 
213 many laws relating division to addition, multiplication, etc.; 
216 many laws relating division to addition, multiplication, etc.; 
214 
217 
215 * ZF/Induct: new directory for examples of inductive definitions, including theory 
218 * ZF/Induct: new directory for examples of inductive definitions, 
216 Multiset for multiset orderings; 
219 including theory Multiset for multiset orderings; 
217 
220 
218 * ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a typeless 
221 * ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a 
219 version of the formalism; 
222 typeless version of the formalism; 
220 
223 
221 
224 
222 *** General *** 
225 *** General *** 
223 
226 
224 * kernel: metalevel proof terms (by Stefan Berghofer), see also ref 
227 * kernel: metalevel proof terms (by Stefan Berghofer), see also ref 