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