src/ZF/Arith.thy
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-10-10 wenzelm 2015-10-10 tuned syntax -- more symbols;
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-07-23 wenzelm 2015-07-23 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-11-01 wenzelm 2014-11-01 eliminated spurious semicolons;
2012-03-06 paulson 2012-03-06 Using mathematical notation for <-> and cardinal arithmetic
2012-03-06 paulson 2012-03-06 mathematical symbols instead of ASCII
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2010-03-13 wenzelm 2010-03-13 removed old CVS Ids; tuned headers;
2007-10-07 wenzelm 2007-10-07 modernized specifications; removed legacy ML bindings;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-09-17 paulson 2004-09-17 converted ZF/Induct/Multiset to Isar script
2003-06-20 paulson 2003-06-20 Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
2003-01-23 paulson 2003-01-23 tidying (by script)
2002-07-16 paulson 2002-07-16 new lemmas
2002-07-14 paulson 2002-07-14 improved presentation markup
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