2012-08-22 ago prefer ML_file over old uses;
2012-03-15 ago merged
2012-03-15 ago replacing ":" by "\<in>"
2012-03-15 ago declare command keywords via theory header, including strict checking outside Pure;
2012-03-06 ago Using mathematical notation for <-> and cardinal arithmetic
2012-03-06 ago mathematical symbols instead of ASCII
2011-11-23 ago modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-11-20 ago eliminated obsolete "standard";
2009-10-17 ago eliminated hard tabulators, guessing at each author's individual tab-width;
2007-10-07 ago modernized specifications;
2005-06-17 ago migrated theory headers to new format
2004-07-30 ago tuned dependencies;
2004-06-08 ago Groups, Rings and supporting lemmas
2003-08-19 ago new case_tac
2003-01-15 ago more new-style theories
2002-08-28 ago various new lemmas for Constructible
2002-07-14 ago Removal of mono.thy
2002-07-14 ago improved presentation markup
2002-06-29 ago conversion of many files to Isar format
2001-10-14 ago moved rulify to ObjectLogic;
2000-09-07 ago tuned ML code (the_context, bind_thms(s));
2000-08-10 ago installation of cancellation simprocs for the integers
1999-01-27 ago new typechecking solver for the simplifier
1997-10-17 ago obselete 'end' hack;
1997-04-02 ago Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
1997-01-03 ago Implicit simpsets and clasets for FOL and ZF
1993-11-16 ago made pseudo theories for all ML files;