src/ZF/Main.thy
2010-03-13 wenzelm 2010-03-13 removed old CVS Ids; tuned headers;
2008-02-11 wenzelm 2008-02-11 added Id;
2008-02-11 krauss 2008-02-11 Made theory names in ZF disjoint from HOL theory names to allow loading both developments in a single session (but not merge them).
2007-10-07 wenzelm 2007-10-07 modernized specifications; removed legacy ML bindings;
2007-04-26 wenzelm 2007-04-26 removed lagacy ML files;
2005-10-17 wenzelm 2005-10-17 moved pos/negDivAlg_induct declarations to Integ/IntDiv.thy; change_simpset;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2002-11-05 paulson 2002-11-05 new operator transrec3
2002-07-19 paulson 2002-07-19 A couple of new theorems for Constructible
2002-07-14 paulson 2002-07-14 improved presentation markup
2002-06-05 paulson 2002-06-05 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
2002-05-17 paulson 2002-05-17 New theorems from Constructible, and moving some Isar material from Main
2002-01-21 paulson 2002-01-21 lexical tidying
2002-01-16 paulson 2002-01-16 Isar version of AC
2002-01-08 paulson 2002-01-08 Added some simprules proofs. Converted theories CardinalArith and OrdQuant to Isar style
2002-01-03 paulson 2002-01-03 Some new theorems for ordinals
2001-12-19 paulson 2001-12-19 separation of the AC part of Main into Main_ZFC, plus a few new lemmas
2001-12-08 wenzelm 2001-12-08 new-style theory; proper declarations of various induction rules;
2000-08-11 paulson 2000-08-11 new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
2000-08-10 paulson 2000-08-10 installation of cancellation simprocs for the integers
2000-06-28 paulson 2000-06-28 finally theory Bin (the integers) is included
1998-09-22 paulson 1998-09-22 deleted erroneous semicolon
1998-07-17 paulson 1998-07-17 as in HOL