src/ZF/List.thy
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2003-06-27 paulson 2003-06-27 Conversion of AllocBase to new-style
2003-06-02 paulson 2003-06-02 Further tweaks of ZF/UNITY
2003-05-27 paulson 2003-05-27 updating ZF-UNITY with Sidi's new material
2003-01-23 paulson 2003-01-23 tidying (by script)
2002-10-01 paulson 2002-10-01 Numerous cosmetic changes, prompted by the new simplifier
2002-09-30 berghofe 2002-09-30 Adapted to new simplifier.
2002-08-27 wenzelm 2002-08-27 *** empty log message ***
2002-08-21 paulson 2002-08-21 new lemmas
2002-07-19 paulson 2002-07-19 A couple of new theorems for Constructible
2002-07-18 paulson 2002-07-18 new theorems to support Constructible proofs
2002-07-14 paulson 2002-07-14 improved presentation markup
2002-07-10 paulson 2002-07-10 Fixed quantified variable name preservation for ball and bex (bounded quants) Requires tweaking of other scripts. Also routine tidying.
2002-07-09 paulson 2002-07-09 converted List to new-style
2002-01-17 paulson 2002-01-17 new definitions from Sidi Ehmety
2000-08-07 paulson 2000-08-07 instantiated Cancel_Numerals for "nat" in ZF
2000-08-01 paulson 2000-08-01 natify, a coercion to reduce the number of type constraints in arithmetic
1999-01-07 paulson 1999-01-07 ZF: the natural numbers as a datatype
1998-12-28 paulson 1998-12-28 new inductive, datatype and primrec packages, etc.
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-01-23 wenzelm 1997-01-23 turned some consts into syntax;
1996-08-20 paulson 1996-08-20 Addition of function set_of_list
1996-06-17 paulson 1996-06-17 Converted to use constdefs instead of defs
1996-02-06 clasohm 1996-02-06 expanded tabs
1995-12-09 clasohm 1995-12-09 removed quotes from consts and syntax sections
1994-12-19 lcp 1994-12-19 removed quotes around "Datatype", and removed needless mention of [Q]Univ
1994-11-29 lcp 1994-11-29 replaced "rules" by "defs"
1994-09-06 lcp 1994-09-06 removal of needless quotes
1994-08-12 lcp 1994-08-12 installation of new inductive/datatype sections
1994-06-21 lcp 1994-06-21 Addition of cardinals and order types, various tidying
1993-11-16 clasohm 1993-11-16 made pseudo theories for all ML files; documented dependencies between all thy and ML files