2011-11-23 ago modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-09-17 ago dropped unused argument – avoids problem with SML/NJ
2011-08-08 ago misc tuning -- eliminated old-fashioned rep_thm;
2010-12-20 ago proper identifiers for consts and types;
2010-12-02 ago renamed trace_simp to simp_trace, and debug_simp to simp_debug;
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 more antiquotations
2010-02-28 ago more antiquotations;
2010-02-27 ago modernized structure Term_Ord;
2009-10-29 ago standardized filter/filter_out;
2009-07-23 ago more @{theory} antiquotations;
2008-12-31 ago moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
2008-03-15 ago proper antiquotations;
2007-10-07 ago modernized specifications;
2007-09-18 ago simplified type int (eliminated, integer);
2006-08-05 ago tuned;
2006-07-12 ago simplified prove_conv;
2006-07-08 ago simprocs: no theory argument -- use simpset context instead;
2006-03-11 ago got rid of type;
2006-01-14 ago sane ERROR handling;
2005-12-01 ago simprocs: static evaluation of simpset;
2005-10-21 ago Goal.prove;
2005-10-17 ago Simplifier.inherit_context instead of Simplifier.inherit_bounds;
2005-08-01 ago simprocs: Simplifier.inherit_bounds;
2005-05-16 ago Use of instead of int in most numeric simprocs; avoids
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-02-15 ago Polymorphic treatment of binary arithmetic using axclasses
2002-08-08 ago tuned;
2002-08-06 ago sane interface for simprocs;
2002-06-29 ago conversion of many files to Isar format
2002-05-16 ago converting Ordinal.ML to Isar format
2002-05-09 ago fixed simproc bug
2001-11-15 ago no handle ERROR;
2001-11-10 ago use Tactic.prove;
2000-09-06 ago bug fix for arithmetic simprocs (nat & int)
2000-08-18 ago simproc bug fix: only TYPING assumptions are given to the simplifier
2000-08-10 ago installation of cancellation simprocs for the integers
2000-08-07 ago instantiated Cancel_Numerals for "nat" in ZF