src/HOL/Integ/int_factor_simprocs.ML
2005-12-20 haftmann 2005-12-20 resolved shadowing of Library.find_first
2005-12-01 wenzelm 2005-12-01 simprocs: static evaluation of simpset;
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;
2004-10-29 paulson 2004-10-29 fixed some awkward problems with nat/int simprocs
2004-05-11 obua 2004-05-11 changes made due to new Ring_and_Field theory
2004-03-02 paulson 2004-03-02 fixed bugs in the setup of arithmetic procedures
2004-02-17 paulson 2004-02-17 further tweaks to the numeric theories
2004-02-15 paulson 2004-02-15 Polymorphic treatment of binary arithmetic using axclasses
2004-02-10 paulson 2004-02-10 generic of_nat and of_int functions, and generalization of iszero and neg
2003-07-15 paulson 2003-07-15 Fixing a simproc bug
2002-08-08 wenzelm 2002-08-08 tuned prove_conv (error reporting done within meta_simplifier.ML);
2002-08-06 wenzelm 2002-08-06 sane interface for simprocs;
2001-11-02 paulson 2001-11-02 Numerals and simprocs for types real and hypreal. The abstract constants 0, 1 and binary numerals work harmoniously.
2001-10-22 paulson 2001-10-22 Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly.
2001-10-06 wenzelm 2001-10-06 * sane numerals (stage 2): plain "num" syntax (removed "#");
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2000-12-21 paulson 2000-12-21 simproc bug fix: negative literals and large terms
2000-12-19 paulson 2000-12-19 inserting the simproc int_cancel_factor
2000-11-29 paulson 2000-11-29 invoking CancelNumeralFactorFun