src/ZF/equalities.thy
2012-03-06 ago Using mathematical notation for <-> and cardinal arithmetic
2012-03-06 ago mathematical symbols instead of ASCII
2011-11-20 ago eliminated obsolete "standard";
2011-05-13 ago proper Proof.context for classical tactics;
2010-03-13 ago removed old CVS Ids;
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-08-28 ago Extended the notion of letter and digit, such that now one may use greek,
2003-07-10 ago Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
2003-06-30 ago Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
2003-06-27 ago Conversion of theory UNITY to Isar script
2003-06-27 ago Conversion of AllocBase to new-style
2003-06-24 ago Converting ZF/UNITY to Isar
2003-05-27 ago updating ZF-UNITY with Sidi's new material
2003-04-23 ago Got rid of the [iff], which was effectively inserting converseD
2002-10-01 ago Numerous cosmetic changes, prompted by the new simplifier
2002-09-30 ago Adapted to new simplifier.
2002-08-28 ago various new lemmas for Constructible
2002-07-14 ago Removal of mono.thy
2002-07-14 ago improved presentation markup
2002-06-29 ago conversion of many files to Isar format
2002-06-26 ago new theorems
2002-06-05 ago Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
2002-05-24 ago new quantifier lemmas
2002-05-22 ago more tidying
2002-05-22 ago tidying up
2002-05-21 ago conversion of OrdQuant.ML to Isar
2002-05-21 ago converted domrange to Isar and merged with equalities
2002-05-20 ago conversion of equalities and WF to Isar
1997-01-03 ago Implicit simpsets and clasets for FOL and ZF
1994-08-15 ago ZF/equalities/Sigma_cons: new
1993-11-16 ago made pseudo theories for all ML files;