src/HOL/Integ/nat_simprocs.ML
2006-01-19 ago setup: theory -> theory;
2005-12-20 ago resolved shadowing of Library.find_first
2005-12-01 ago simprocs: static evaluation of simpset;
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 IntInf.int instead of int in most numeric simprocs; avoids
2005-05-04 ago Fixing a problem with lin.arith.
2004-10-29 ago fixed some awkward problems with nat/int simprocs
2004-03-19 ago New simplification ordering to move numerals together. Fixes a bug in the
2004-03-04 ago new material from Avigad, and simplified treatment of division by 0
2004-02-17 ago further tweaks to the numeric theories
2004-02-15 ago Polymorphic treatment of binary arithmetic using axclasses
2004-01-28 ago tidying up arithmetic for the hyperreals
2004-01-27 ago replacing HOL/Real/PRat, PNat by the rational number development
2003-12-04 ago further simplifications of the integer development; converting more .ML files
2003-11-25 ago More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
2002-08-08 ago tuned prove_conv (error reporting done within meta_simplifier.ML);
2002-08-06 ago sane interface for simprocs;
2002-02-26 ago Fixed the natxx_cancel_numerals simprocs so that they pull out Sucs and
2001-12-01 ago renamed class "term" to "type" (actually "HOL.type");
2001-11-15 ago new theories from Jacques Fleuriot
2001-10-22 ago Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
2001-10-06 ago * sane numerals (stage 2): plain "num" syntax (removed "#");
2001-10-05 ago sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
2001-06-25 ago Simprocs for type "nat" no longer introduce numerals unless they are already
2001-05-31 ago Allow Suc-numerals as coefficients in lin-arith formulae
2001-05-11 ago mult_Suc generally, not just for numerals.
2001-05-11 ago added mult_Suc laws to lin.arith.simpset.
2001-04-19 ago *** empty log message ***
2001-01-12 ago HOLogic.dest_binum;
2000-12-19 ago inserting the simproc nat_cancel_factor
2000-12-18 ago moved mk_bin from Numerals to HOLogic
2000-12-01 ago Linear arithmetic now copes with mixed nat/int formulae.
2000-11-29 ago invoking CancelNumeralFactorFun
2000-08-10 ago new structure field "add" for CombineNumerals
2000-08-07 ago added a dummy "thm list" argument to prove_conv for the new interface to
2000-07-25 ago rearranged setup of arithmetic procedures, avoiding global reference values;