src/ZF/Datatype_ZF.thy
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2013-11-11 wenzelm 2013-11-11 tuned signature -- removed obsolete Addsimprocs, Delsimprocs;
2013-05-11 wenzelm 2013-05-11 prefer explicitly qualified exceptions, which is particular important for robust handlers;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2011-02-18 wenzelm 2011-02-18 more precise headers;
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-08-18 haftmann 2010-08-18 deglobalization
2010-02-28 wenzelm 2010-02-28 more antiquotations; eliminated legacy ML bindings;
2009-09-29 wenzelm 2009-09-29 modernized Balanced_Tree;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-08-28 wenzelm 2009-08-28 modernized messages -- eliminated ctyp/cterm operations;
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2008-09-17 wenzelm 2008-09-17 back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-03-29 wenzelm 2008-03-29 replaced 'ML_setup' by 'ML';
2008-02-11 krauss 2008-02-11 Made theory names in ZF disjoint from HOL theory names to allow loading both developments in a single session (but not merge them).