2002-07-09 paulson 2002-07-09 better document preparation
2002-05-28 paulson 2002-05-28 deleted some useless ML bindings
2002-05-22 paulson 2002-05-22 new version of nat_case, nat_case3
2002-05-18 paulson 2002-05-18 converted Arith, Univ, func to Isar format!
2001-11-09 wenzelm 2001-11-09 eliminated old "symbols" syntax, use "xsymbols" instead;
2000-09-15 wenzelm 2000-09-15 tuned symbols;
2000-08-24 paulson 2000-08-24 added some xsymbols, and tidied
2000-08-18 paulson 2000-08-18 X-symbols for ordinal, cardinal, integer arithmetic
2000-08-01 paulson 2000-08-01 used natify with div and mod; also put in the divide-by-zero trick
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
1997-10-10 wenzelm 1997-10-10 fixed dots;
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
1994-11-29 lcp 1994-11-29 replaced "rules" by "defs"
1993-11-16 clasohm 1993-11-16 made pseudo theories for all ML files; documented dependencies between all thy and ML files
1993-10-05 lcp 1993-10-05 ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many changes epsilon,arith: many changes ordinal/succ_mem_succI/E: deleted; use succ_leI/E nat/nat_0_in_succ: deleted; use nat_0_le univ/Vset_rankI: deleted; use VsetI
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