src/Provers/Arith/cancel_numerals.ML
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2013-11-23 wenzelm 2013-11-23 tuned;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2011-09-17 haftmann 2011-09-17 dropped unused argument – avoids problem with SML/NJ
2011-06-29 wenzelm 2011-06-29 tuned signature;
2011-04-22 wenzelm 2011-04-22 tuned signature;
2010-03-13 wenzelm 2010-03-13 removed old CVS Ids; tuned headers;
2007-09-18 wenzelm 2007-09-18 simplified type int (eliminated IntInf.int, integer);
2006-07-12 wenzelm 2006-07-12 prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars; tuned;
2006-07-08 wenzelm 2006-07-08 simprocs: no theory argument -- use simpset context instead;
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-01 wenzelm 2005-09-01 curried_lookup/update; tuned;
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-07-08 wenzelm 2004-07-08 adapted type of simprocs;
2004-02-15 paulson 2004-02-15 Polymorphic treatment of binary arithmetic using axclasses
2002-08-08 wenzelm 2002-08-08 adhoc_freeze_vars;
2000-08-07 paulson 2000-08-07 prove_conv gets an extra argument, so the ZF instantiation can use hyps
2000-06-29 paulson 2000-06-29 now freezes Vars in order to prevent errors in cases like these: Goal "Suc (x + i + j) + ?q ?ii ?jj + k + x = xxx"; Goal "Suc (x + i + j) = x + f(?q i j) + k"; Goal "Suc (x + i + j) = x + ?q i j + k"; Goal "Suc (?q ?ii ?jj + i + j) + ?rq ?ii ?jj + k + ?q ?ii ?jj = xxx";
2000-05-05 paulson 2000-05-05 simprocs now simplify the RHS of their result
2000-05-02 paulson 2000-05-02 various bug fixes
2000-04-28 paulson 2000-04-28 inserted triviality check
2000-04-21 paulson 2000-04-21 now works for coefficients, not just for numerals no longer works by subtraction, so no need for inverse_fold
2000-04-18 paulson 2000-04-18 new simprocs for numerals of type "nat"