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;
2012-03-15 ago declare minor keywords via theory header;
2012-03-06 ago Using mathematical notation for <-> and cardinal arithmetic
2010-08-18 ago deglobalization
2009-01-21 ago dropped ID
2008-03-29 ago replaced 'ML_setup' by 'ML';
2008-03-01 ago tuned ML code, more antiquotations;
2008-03-01 ago misc cleanup of embedded ML code;
2008-02-11 ago Made theory names in ZF disjoint from HOL theory names to allow loading both developments