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