src/ZF/OrdQuant.thy
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2003-02-06 paulson 2003-02-06 changed ** to ## to avoid conflict with new comment syntax
2002-10-01 paulson 2002-10-01 Numerous cosmetic changes, prompted by the new simplifier
2002-08-06 wenzelm 2002-08-06 sane interface for simprocs;
2002-07-16 paulson 2002-07-16 tweaked definition of setclass
2002-07-10 paulson 2002-07-10 Fixed quantified variable name preservation for ball and bex (bounded quants) Requires tweaking of other scripts. Also routine tidying.
2002-07-05 paulson 2002-07-05 fixed precedences of **
2002-07-04 paulson 2002-07-04 Constructible: some separation axioms
2002-07-04 paulson 2002-07-04 miniscoping for class-bounded quantifiers (rall and rex)
2002-06-28 paulson 2002-06-28 added class quantifiers
2002-06-24 paulson 2002-06-24 moving some results around
2002-05-23 paulson 2002-05-23 new definition of "apply" and new simprule "beta_if"
2002-05-22 paulson 2002-05-22 more tidying
2002-05-22 paulson 2002-05-22 tidying up
2002-05-22 paulson 2002-05-22 tidied
2002-05-21 paulson 2002-05-21 conversion of OrdQuant.ML to Isar
2002-05-17 paulson 2002-05-17 New theorems from Constructible, and moving some Isar material from Main
2002-05-15 paulson 2002-05-15 better simplification of trivial existential equalities
2002-05-08 paulson 2002-05-08 new lemmas
2002-01-21 paulson 2002-01-21 new simprules and classical rules
2002-01-21 paulson 2002-01-21 lexical tidying
2002-01-15 paulson 2002-01-15 now [rule_format] knows about ospec
2002-01-08 paulson 2002-01-08 Added some simprules proofs. Converted theories CardinalArith and OrdQuant to Isar style
2002-01-03 paulson 2002-01-03 Some new theorems for ordinals
2001-12-19 paulson 2001-12-19 separation of the AC part of Main into Main_ZFC, plus a few new lemmas
2001-11-09 wenzelm 2001-11-09 eliminated old "symbols" syntax, use "xsymbols" instead;
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-23 wenzelm 1997-01-23 added symbols syntax;
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF