src/ZF/Zorn.thy
2015-12-30 wenzelm 2015-12-30 clarified syntax;
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-07-23 wenzelm 2015-07-23 isabelle update_cartouches;
2015-03-23 wenzelm 2015-03-23 prefer local fixes;
2014-11-02 wenzelm 2014-11-02 modernized header;
2012-03-06 paulson 2012-03-06 mathematical symbols instead of ASCII
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2008-07-29 ballarin 2008-07-29 Zorn's Lemma for partial orders.
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
2004-04-22 wenzelm 2004-04-22 constdefs: proper order;
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.
2003-01-23 paulson 2003-01-23 tidying (by script)
2002-09-03 paulson 2002-09-03 tidied
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-05-23 paulson 2002-05-23 new definition of "apply" and new simprule "beta_if"
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.
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-12-19 lcp 1994-12-19 removed quotes around "Inductive"
1994-11-29 lcp 1994-11-29 replaced "rules" by "defs"
1994-08-25 lcp 1994-08-25 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without the keyword "inductive" making the theory file fail ZF/Makefile: now has Inductive.thy,.ML ZF/Datatype,Finite,Zorn: depend upon Inductive ZF/intr_elim: now checks that the inductive name does not clash with existing theory names ZF/ind_section: deleted things replicated in Pure/section_utils.ML ZF/ROOT: now loads Pure/section_utils
1994-08-12 lcp 1994-08-12 installation of new inductive/datatype sections
1994-07-26 lcp 1994-07-26 Axiom of choice, cardinality results, etc.