src/ZF/Finite.thy
2012-03-15 ago replacing ":" by "\<in>"
2012-03-06 ago Using mathematical notation for <-> and cardinal arithmetic
2012-03-06 ago mathematical symbols instead of ASCII
2012-02-14 ago prefer high-level elim_format;
2011-11-20 ago eliminated obsolete "standard";
2009-10-17 ago eliminated hard tabulators, guessing at each author's individual tab-width;
2008-02-11 ago Made theory names in ZF disjoint from HOL theory names to allow loading both developments
2007-10-07 ago modernized specifications;
2005-06-17 ago migrated theory headers to new format
2004-06-08 ago Groups, Rings and supporting lemmas
2003-01-23 ago tidying (by script)
2002-10-01 ago Numerous cosmetic changes, prompted by the new simplifier
2002-08-27 ago *** empty log message ***
2002-07-14 ago improved presentation markup
2002-07-09 ago better document preparation
2002-07-02 ago Tidying and introduction of various new theorems
2002-06-05 ago Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
2002-05-31 ago conversion of Finite to Isar format
2001-11-15 ago depends on Epsilon!
2001-11-13 ago rearranged inductive package for Isar;
2000-08-01 ago natify, a coercion to reduce the number of type constraints in arithmetic
1998-12-28 ago new inductive, datatype and primrec packages, etc.
1996-02-06 ago expanded tabs
1995-12-09 ago removed quotes from consts and syntax sections
1995-06-22 ago removed \...\ inside strings
1994-12-19 ago removed quotes around "Inductive"
1994-08-25 ago ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
1994-08-16 ago ZF/Finite: added the finite function space, A-||>B
1994-08-12 ago installation of new inductive/datatype sections