src/ZF/AC.thy
2017-04-09 wenzelm 2017-04-09 clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
2015-12-30 wenzelm 2015-12-30 clarified syntax;
2015-07-23 wenzelm 2015-07-23 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2012-03-15 paulson 2012-03-15 replacing ":" by "\<in>"
2012-03-06 paulson 2012-03-06 mathematical symbols instead of ASCII
2010-03-13 wenzelm 2010-03-13 removed old CVS Ids; tuned headers;
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;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2003-08-28 skalberg 2003-08-28 Extended the notion of letter and digit, such that now one may use greek, gothic, euler, or calligraphic letters as normal letters.
2002-07-09 paulson 2002-07-09 better document preparation
2002-07-02 paulson 2002-07-02 Tidying and introduction of various new theorems
2002-05-15 paulson 2002-05-15 better simplification of trivial existential equalities
2002-05-10 paulson 2002-05-10 converted the AC branch to Isar
1998-12-28 paulson 1998-12-28 new inductive, datatype and primrec packages, etc.
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF
1996-02-06 clasohm 1996-02-06 expanded tabs
1994-07-26 lcp 1994-07-26 Axiom of choice, cardinality results, etc.