2012-08-22 ago prefer ML_file over old uses;
2011-11-20 ago eliminated obsolete "standard";
2011-11-20 ago tuned;
2011-08-10 ago old term operations are legacy;
2011-05-14 ago modernized functor names;
2011-05-02 ago added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
2010-12-20 ago proper identifiers for consts and types;
2010-09-20 ago renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-08-27 ago proper configuration option "show_proofs";
2010-08-18 ago deglobalization
2010-04-28 ago renamed command 'defaultsort' to 'default_sort';
2010-04-23 ago mark schematic statements explicitly;
2010-02-15 ago eliminated unnamed infixes;
2010-02-11 ago modernized translations;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-01-02 ago fixed assumption proof;
2008-12-31 ago moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
2008-06-11 ago changed pred_congs: merely cover pred1_cong pred2_cong pred3_cong;
2008-06-11 ago tuned comments;
2008-05-18 ago setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;
2008-03-29 ago replaced 'ML_setup' by 'ML';
2008-03-18 ago converted legacy ML scripts;
2005-09-18 ago converted to Isar theory format;
2004-06-01 ago removed obsolete sort 'logic';
1999-04-26 ago fixed a bug many years old in rule plusEC
1997-10-20 ago adapted to qualified names;
1997-10-10 ago fixed dots;
1997-03-04 ago Removed needless quotes
1996-02-05 ago expanded tabs
1995-06-21 ago removed \...\ inside strings
1995-06-02 ago Corrected comments in headers
1994-10-21 ago FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
1994-03-17 ago new type declaration syntax instead of numbers
1993-09-16 ago Initial revision