2012-08-08 ago proper axiomatization of "mem" -- do not leave it formally unspecified;
2012-07-24 ago clarified "this_name" vs. former "reset" feature -- imitate the latter by loading other session sources directly;
2012-03-16 ago modernized axiomatization;
2012-03-13 ago Structured proofs concerning the square of an infinite cardinal
2012-03-06 ago mathematical symbols instead of ASCII
2012-03-01 ago Removal of obsolete ML bindings
2011-11-20 ago eliminated obsolete "standard";
2011-08-11 ago redundant use of misc_legacy.ML;
2011-02-18 ago modernized specifications;
2010-12-20 ago proper identifiers for consts and types;
2010-12-17 ago replaced command 'nonterminals' by slightly modernized version 'nonterminal';
2010-11-26 ago prefer non-classical eliminations in Pure reasoning, notably "rule" steps;
2010-09-03 ago turned eta_contract into proper configuration option;
2010-08-27 ago expanded some aliases from structure Unsynchronized;
2010-08-18 ago deglobalization
2010-07-12 ago moved misc legacy stuff from OldGoals to Misc_Legacy;
2010-06-11 ago avoid references to old constdefs
2010-02-11 ago numeral syntax: clarify parse trees vs. actual terms;
2010-02-10 ago modernized translations;
2009-10-17 ago eliminated hard tabulators, guessing at each author's individual tab-width;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2008-07-29 ago Lemmas added
2007-10-07 ago modernized specifications;
2007-10-03 ago avoid unnamed infixes;
2007-05-31 ago tuned ML setup;
2006-01-29 ago declare atomize/defn for Ball;
2005-12-15 ago removed obsolete/unused setup_induction;
2005-10-07 ago replaced _K by dummy abstraction;
2005-06-17 ago migrated theory headers to new format
2005-02-01 ago the new subst tactic, by Lucas Dixon
2004-06-08 ago Groups, Rings and supporting lemmas
2004-06-01 ago removed obsolete sort 'logic';
2004-04-14 ago use more symbols in HTML output
2003-10-10 ago finalconsts
2003-07-10 ago Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
2003-06-27 ago Conversion of AllocBase to new-style
2003-01-15 ago more new-style theories
2002-05-23 ago new definition of "apply" and new simprule "beta_if"
2002-05-13 ago quotes around types
2002-05-08 ago the new predicate "relation"
2002-05-07 ago tuned;
2002-02-15 ago a new definition of "restrict"
2002-01-15 ago split can now be unfolded even with one argument
2001-12-19 ago separation of the AC part of Main into Main_ZFC, plus a few new lemmas
2001-11-09 ago eliminated old "symbols" syntax, use "xsymbols" instead;
2001-05-21 ago fixed the X-symbol syntax for lambda
2001-03-30 ago the one-point rule for bounded quantifiers
2000-09-15 ago tuned spacing of symbols syntax;
2000-08-24 ago added some xsymbols, and tidied
1999-03-10 ago HTML output;
1999-01-07 ago if-then-else syntax for ZF
1997-10-20 ago local;
1997-10-16 ago global;
1997-10-10 ago fixed dots;
1997-09-22 ago tuned pattern syntax;
1997-04-29 ago deactivated new symbols (not yet printable on xterm, emacs);
1997-04-29 ago added \<langle>, \<rangle> symbols syntax;
1997-04-02 ago Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
1997-01-23 ago added symbols syntax;
1997-01-03 ago Implicit simpsets and clasets for FOL and ZF