src/ZF/QPair.thy
2014-11-02 wenzelm 2014-11-02 modernized header;
2012-03-15 paulson 2012-03-15 replacing ":" by "\<in>"
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-20 wenzelm 2011-11-20 eliminated obsolete "standard";
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;
2007-04-26 wenzelm 2007-04-26 eliminated unnamed infixes, tuned syntax;
2005-10-07 wenzelm 2005-10-07 replaced _K by dummy abstraction;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2003-02-19 paulson 2003-02-19 fixed anomalies in the installed classical rules
2003-01-23 paulson 2003-01-23 tidying (by script)
2002-10-01 paulson 2002-10-01 Numerous cosmetic changes, prompted by the new simplifier
2002-08-28 paulson 2002-08-28 various new lemmas for Constructible
2002-08-27 wenzelm 2002-08-27 avoid duplicate fact bindings;
2002-07-14 paulson 2002-07-14 Removal of mono.thy
2002-07-14 paulson 2002-07-14 improved presentation markup
2002-07-02 paulson 2002-07-02 conversion of QPair to Isar
2002-06-29 paulson 2002-06-29 conversion of many files to Isar format
2002-06-18 paulson 2002-06-18 tidying
1999-01-12 wenzelm 1999-01-12 eliminated global/local names;
1997-10-20 wenzelm 1997-10-20 local;
1997-10-17 wenzelm 1997-10-17 global;
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF
1996-02-06 clasohm 1996-02-06 expanded tabs
1995-12-09 clasohm 1995-12-09 removed quotes from consts and syntax sections
1995-05-03 lcp 1995-05-03 Changed definitions so that qsplit is now defined in terms of qfst, qsnd. AT PRESENT THERE IS NO PATTERN-MATCHING FOR QSPLIT.
1995-03-07 lcp 1995-03-07 Moved declarations of @QSUM and <*> to a syntax section. Changed print_translation because <*> is now an infix.
1994-11-29 lcp 1994-11-29 replaced "rules" by "defs"
1994-08-12 lcp 1994-08-12 installation of new inductive/datatype sections
1994-06-21 lcp 1994-06-21 Addition of cardinals and order types, various tidying
1993-11-16 clasohm 1993-11-16 made pseudo theories for all ML files; documented dependencies between all thy and ML files
1993-11-15 lcp 1993-11-15 changed all co- and co_ to co ZF/ex/llistfn: new coinduction example: flip ZF/ex/llist_eq: now uses standard pairs not qpairs
1993-10-08 wenzelm 1993-10-08 added parse rule for "<*>"; removed ndependent_tr;
1993-09-16 clasohm 1993-09-16 Initial revision