src/ZF/OrdQuant.thy
2011-02-18 wenzelm 2011-02-18 more precise headers;
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-04-29 wenzelm 2010-04-29 proper context for mksimps etc. -- via simpset of the running Simplifier;
2010-02-11 wenzelm 2010-02-11 numeral syntax: clarify parse trees vs. actual terms; modernized translations; formal markup of @{syntax_const} and @{const_syntax};
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2008-09-17 wenzelm 2008-09-17 back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-03-29 wenzelm 2008-03-29 replaced 'ML_setup' by 'ML';
2008-03-19 wenzelm 2008-03-19 eliminated change_claset/simpset;
2007-10-07 wenzelm 2007-10-07 modernized specifications; removed legacy ML bindings;
2005-12-01 wenzelm 2005-12-01 unfold_tac: static evaluation of simpset;
2005-10-17 wenzelm 2005-10-17 change_claset/simpset;
2005-08-02 wenzelm 2005-08-02 simprocs: Simplifier.inherit_bounds;
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