src/ZF/Ordinal.thy
2012-03-17 ago tidying and structured proofs
2012-03-15 ago beautification and structured proofs
2012-03-15 ago replacing ":" by "\<in>"
2012-03-14 ago structured case and induct rules
2012-03-14 ago rationalising the induction rule trans_induct3
2012-03-08 ago Structured and calculation-based proofs (with new trans rules!)
2012-03-06 ago mathematical symbols instead of ASCII
2010-03-13 ago removed old CVS Ids;
2007-10-07 ago modernized specifications;
2007-04-26 ago eliminated unnamed infixes, tuned syntax;
2005-06-17 ago migrated theory headers to new format
2004-06-02 ago new rules for simplifying quantifiers with Sigma
2004-04-14 ago use more symbols in HTML output
2003-01-23 ago tidying (by script)
2002-10-01 ago Numerous cosmetic changes, prompted by the new simplifier
2002-08-28 ago various new lemmas for Constructible
2002-08-27 ago avoid duplicate fact bindings;
2002-07-19 ago A couple of new theorems for Constructible
2002-07-14 ago improved presentation markup
2002-07-02 ago Tidying and introduction of various new theorems
2002-06-24 ago new lemmas
2002-06-05 ago Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
2002-05-22 ago tidying up
2002-05-17 ago New theorems from Constructible, and moving some Isar material from Main
2002-05-16 ago converting Ordinal.ML to Isar format
2001-11-09 ago eliminated old "symbols" syntax, use "xsymbols" instead;
1997-01-23 ago added symbols syntax;
1997-01-23 ago turned some consts into syntax;
1997-01-03 ago Implicit simpsets and clasets for FOL and ZF
1996-02-06 ago expanded tabs
1995-12-09 ago removed quotes from consts and syntax sections
1995-01-12 ago Now depends upon Bool, so that 1 and 2 are defined
1994-11-29 ago replaced "rules" by "defs"
1994-06-21 ago Addition of cardinals and order types, various tidying