src/Provers/Arith/combine_numerals.ML
2010-03-13 wenzelm 2010-03-13 removed old CVS Ids; tuned headers;
2007-05-21 huffman 2007-05-21 generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
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;
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-18 paulson 2000-08-18 now allows dest_coeff to fail
2000-08-10 paulson 2000-08-10 new structure field "add" for CombineNumerals
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 wenzelm 2000-05-05 removed dead code: listof;
2000-05-05 paulson 2000-05-05 simprocs now simplify the RHS of their result
2000-05-02 paulson 2000-05-02 new simproc, replacing combine_coeffs and working for nat, int, real