src/ZF/pair.thy
2012-08-22 ago prefer ML_file over old uses;
2012-03-15 ago replacing ":" by "\<in>"
2012-03-08 ago Structured and calculation-based proofs (with new trans rules!)
2012-03-06 ago Using mathematical notation for <-> and cardinal arithmetic
2012-03-06 ago mathematical symbols instead of ASCII
2011-11-24 ago modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-11-23 ago modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-11-20 ago eliminated obsolete "standard";
2011-05-13 ago clarified map_simpset versus Simplifier.map_simpset_global;
2011-05-13 ago make ZF_cs snapshot after final setup;
2011-04-22 ago misc tuning and simplification;
2011-04-22 ago proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
2011-04-22 ago modernized Quantifier1 simproc setup;
2011-02-18 ago more precise headers;
2008-12-03 ago made repository layout more coherent with logical distribution structure; stripped some $Id$s
2007-10-07 ago modernized specifications;
2005-08-02 ago tuned;
2005-06-17 ago migrated theory headers to new format
2004-06-02 ago new rules for simplifying quantifiers with Sigma
2002-08-28 ago various new lemmas for Constructible
2002-07-14 ago Removal of mono.thy
2002-06-23 ago conversion of Sum, pair to Isar script
2001-10-05 ago tuned;
2000-08-10 ago installation of cancellation simprocs for the integers
1997-01-03 ago Implicit simpsets and clasets for FOL and ZF
1993-11-16 ago made pseudo theories for all ML files;