src/ZF/equalities.thy
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2010-03-13 wenzelm 2010-03-13 removed old CVS Ids; tuned headers;
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-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-07-10 paulson 2003-07-10 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new variable
2003-06-30 paulson 2003-06-30 Removal of UNITY/UNITYMisc, moving its theorems elsewhere. Conversion of UNITY/State to Isar format.;
2003-06-27 paulson 2003-06-27 Conversion of theory UNITY to Isar script
2003-06-27 paulson 2003-06-27 Conversion of AllocBase to new-style
2003-06-24 paulson 2003-06-24 Converting ZF/UNITY to Isar
2003-05-27 paulson 2003-05-27 updating ZF-UNITY with Sidi's new material
2003-04-23 paulson 2003-04-23 Got rid of the [iff], which was effectively inserting converseD
2002-10-01 paulson 2002-10-01 Numerous cosmetic changes, prompted by the new simplifier
2002-09-30 berghofe 2002-09-30 Adapted to new simplifier.
2002-08-28 paulson 2002-08-28 various new lemmas for Constructible
2002-07-14 paulson 2002-07-14 Removal of mono.thy
2002-07-14 paulson 2002-07-14 improved presentation markup
2002-06-29 paulson 2002-06-29 conversion of many files to Isar format
2002-06-26 paulson 2002-06-26 new theorems
2002-06-05 paulson 2002-06-05 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
2002-05-24 paulson 2002-05-24 new quantifier lemmas
2002-05-22 paulson 2002-05-22 more tidying
2002-05-22 paulson 2002-05-22 tidying up
2002-05-21 paulson 2002-05-21 conversion of OrdQuant.ML to Isar
2002-05-21 paulson 2002-05-21 converted domrange to Isar and merged with equalities
2002-05-20 paulson 2002-05-20 conversion of equalities and WF to Isar
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF
1994-08-15 lcp 1994-08-15 ZF/equalities/Sigma_cons: new ZF/equalities/cons_eq: new ZF/equalities.thy: added final newline
1993-11-16 clasohm 1993-11-16 made pseudo theories for all ML files; documented dependencies between all thy and ML files