src/ZF/Nat.thy
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2003-08-19 paulson 2003-08-19 new case_tac
2003-05-30 paulson 2003-05-30 getting ZF/UNITY working again
2003-05-27 paulson 2003-05-27 updating ZF-UNITY with Sidi's new material
2003-02-19 paulson 2003-02-19 fixed anomalies in the installed classical rules
2003-01-23 paulson 2003-01-23 tidying (by script)
2002-10-04 paulson 2002-10-04 Various simplifications of the Constructible theories
2002-08-27 wenzelm 2002-08-27 *** empty log message ***
2002-07-14 paulson 2002-07-14 Removal of mono.thy
2002-07-14 paulson 2002-07-14 improved presentation markup
2002-07-02 paulson 2002-07-02 Tidying and introduction of various new theorems
2002-06-05 paulson 2002-06-05 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
2002-05-28 paulson 2002-05-28 deleted some useless ML bindings
2002-05-22 paulson 2002-05-22 more tidying
2002-05-22 paulson 2002-05-22 new version of nat_case, nat_case3
2002-05-22 paulson 2002-05-22 conversion of Nat to Isar
2002-01-17 paulson 2002-01-17 new definitions from Sidi Ehmety
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF
1996-02-06 clasohm 1996-02-06 expanded tabs
1995-12-09 clasohm 1995-12-09 removed quotes from consts and syntax sections
1995-06-22 clasohm 1995-06-22 removed \...\ inside strings
1994-11-29 lcp 1994-11-29 replaced "rules" by "defs"
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
1993-09-17 lcp 1993-09-17 Installation of new simplifier for ZF. Deleted all congruence rules not involving local assumptions. NB the congruence rules for Sigma and Pi (dependent type constructions) cause difficulties and are not used by default.
1993-09-16 clasohm 1993-09-16 Initial revision