src/ZF/Finite.thy
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 Using mathematical notation for <-> and cardinal arithmetic
2012-03-06 paulson 2012-03-06 mathematical symbols instead of ASCII
2012-02-14 wenzelm 2012-02-14 prefer high-level elim_format;
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-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-06-08 paulson 2004-06-08 Groups, Rings and supporting lemmas
2003-01-23 paulson 2003-01-23 tidying (by script)
2002-10-01 paulson 2002-10-01 Numerous cosmetic changes, prompted by the new simplifier
2002-08-27 wenzelm 2002-08-27 *** empty log message ***
2002-07-14 paulson 2002-07-14 improved presentation markup
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-06-05 paulson 2002-06-05 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
2002-05-31 paulson 2002-05-31 conversion of Finite to Isar format
2001-11-15 wenzelm 2001-11-15 depends on Epsilon!
2001-11-13 wenzelm 2001-11-13 rearranged inductive package for Isar;
2000-08-01 paulson 2000-08-01 natify, a coercion to reduce the number of type constraints in arithmetic
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-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-16 lcp 1994-08-16 ZF/Finite: added the finite function space, A-||>B ZF/InfDatatype: added rules for the above
1994-08-12 lcp 1994-08-12 installation of new inductive/datatype sections