328 laws relating division to addition, multiplication, etc.; |
328 laws relating division to addition, multiplication, etc.; |
329 |
329 |
330 * ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a |
330 * ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a |
331 typeless version of the formalism; |
331 typeless version of the formalism; |
332 |
332 |
333 * ZF/AC, Coind, IMP, Resid: updated and converted to new-style theory format; |
333 * ZF/AC, Coind, IMP, Resid: updated and converted to new-style theory |
|
334 format; |
334 |
335 |
335 * ZF/Induct: new directory for examples of inductive definitions, |
336 * ZF/Induct: new directory for examples of inductive definitions, |
336 including theory Multiset for multiset orderings; converted to |
337 including theory Multiset for multiset orderings; converted to |
337 new-style theory format; |
338 new-style theory format; |
338 |
339 |
339 * Many new theorems about lists, ordinals, etc.; |
340 * ZF: many new theorems about lists, ordinals, etc.; |
340 |
341 |
341 |
342 |
342 *** General *** |
343 *** General *** |
343 |
344 |
344 * Pure/kernel: meta-level proof terms (by Stefan Berghofer); reference |
345 * Pure/kernel: meta-level proof terms (by Stefan Berghofer); reference |