src/ZF/Ordinal.thy
2012-03-06 paulson 2012-03-06 mathematical symbols instead of ASCII
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-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
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
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-19 paulson 2002-07-19 A couple of new theorems for Constructible
2002-07-14 paulson 2002-07-14 improved presentation markup
2002-07-02 paulson 2002-07-02 Tidying and introduction of various new theorems
2002-06-24 paulson 2002-06-24 new lemmas
2002-06-05 paulson 2002-06-05 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
2002-05-22 paulson 2002-05-22 tidying up
2002-05-17 paulson 2002-05-17 New theorems from Constructible, and moving some Isar material from Main
2002-05-16 paulson 2002-05-16 converting Ordinal.ML to Isar format
2001-11-09 wenzelm 2001-11-09 eliminated old "symbols" syntax, use "xsymbols" instead;
1997-01-23 wenzelm 1997-01-23 added symbols syntax;
1997-01-23 wenzelm 1997-01-23 turned some consts into syntax;
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-01-12 lcp 1995-01-12 Now depends upon Bool, so that 1 and 2 are defined
1994-11-29 lcp 1994-11-29 replaced "rules" by "defs"
1994-06-21 lcp 1994-06-21 Addition of cardinals and order types, various tidying