2012-08-22 ago prefer ML_file over old uses;
2012-03-15 ago declare command keywords via theory header, including strict checking outside Pure;
2011-02-18 ago more precise headers;
2010-08-25 ago renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-08-18 ago deglobalization
2010-02-28 ago more antiquotations;
2009-09-29 ago modernized Balanced_Tree;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-08-28 ago modernized messages -- eliminated ctyp/cterm operations;
2009-07-15 ago more antiquotations;
2008-09-17 ago back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 ago structure Display: less pervasive operations;
2008-03-29 ago replaced 'ML_setup' by 'ML';
2008-02-11 ago Made theory names in ZF disjoint from HOL theory names to allow loading both developments