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: new-style 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: meta-level proof terms (by Stefan Berghofer), see also ref |
227 * kernel: meta-level proof terms (by Stefan Berghofer), see also ref |