2012-03-06 ago mathematical symbols instead of ASCII
2011-11-20 ago eliminated obsolete "standard";
2009-10-17 ago eliminated hard tabulators, guessing at each author's individual tab-width;
2008-07-29 ago Zorn's Lemma for partial orders.
2008-02-11 ago Made theory names in ZF disjoint from HOL theory names to allow loading both developments
2007-10-07 ago modernized specifications;
2005-06-17 ago migrated theory headers to new format
2004-04-22 ago constdefs: proper order;
2003-08-28 ago Extended the notion of letter and digit, such that now one may use greek,
2003-01-23 ago tidying (by script)
2002-09-03 ago tidied
2002-07-14 ago improved presentation markup
2002-07-02 ago Tidying and introduction of various new theorems
2002-05-23 ago new definition of "apply" and new simprule "beta_if"
2002-05-10 ago converted the AC branch to Isar
1998-12-28 ago new inductive, datatype and primrec packages, etc.
1996-02-06 ago expanded tabs
1995-12-09 ago removed quotes from consts and syntax sections
1995-06-22 ago removed \...\ inside strings
1994-12-19 ago removed quotes around "Inductive"
1994-11-29 ago replaced "rules" by "defs"
1994-08-25 ago ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
1994-08-12 ago installation of new inductive/datatype sections
1994-07-26 ago Axiom of choice, cardinality results, etc.