equal
deleted
inserted
replaced
298 |
298 |
299 * ZF/Induct: new directory for examples of inductive definitions, |
299 * ZF/Induct: new directory for examples of inductive definitions, |
300 including theory Multiset for multiset orderings; converted to |
300 including theory Multiset for multiset orderings; converted to |
301 new-style theory format; |
301 new-style theory format; |
302 |
302 |
|
303 * Many new theorems about lists, ordinals, etc.; |
|
304 |
303 |
305 |
304 *** General *** |
306 *** General *** |
305 |
307 |
306 * Pure/kernel: meta-level proof terms (by Stefan Berghofer); reference |
308 * Pure/kernel: meta-level proof terms (by Stefan Berghofer); reference |
307 variable proof controls level of detail: 0 = no proofs (only oracle |
309 variable proof controls level of detail: 0 = no proofs (only oracle |