2005-05-16 paulson 2005-05-16 Use of instead of int in most numeric simprocs; avoids integer overflow in SML/NJ
2005-05-04 nipkow 2005-05-04 Fixing a problem with lin.arith.
2004-10-29 paulson 2004-10-29 fixed some awkward problems with nat/int simprocs
2004-03-19 paulson 2004-03-19 New simplification ordering to move numerals together. Fixes a bug in the nat cancellation simprocs
2004-03-04 paulson 2004-03-04 new material from Avigad, and simplified treatment of division by 0
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-01-28 paulson 2004-01-28 tidying up arithmetic for the hyperreals
2004-01-27 paulson 2004-01-27 replacing HOL/Real/PRat, PNat by the rational number development of Markus Wenzel
2003-12-04 paulson 2003-12-04 further simplifications of the integer development; converting more .ML files to Isar scripts
2003-11-25 paulson 2003-11-25 More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas to Isar script.
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;
2002-02-26 paulson 2002-02-26 Fixed the natxx_cancel_numerals simprocs so that they pull out Sucs and return False for e.g. Suc x = 0. Removed ad-hoc lemmas for that purpose.
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-11-15 paulson 2001-11-15 new theories from Jacques Fleuriot
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;
2001-06-25 paulson 2001-06-25 Simprocs for type "nat" no longer introduce numerals unless they are already present in the expression, and in a coefficient position (i.e. as a factor of a monomial).
2001-05-31 nipkow 2001-05-31 Allow Suc-numerals as coefficients in lin-arith formulae
2001-05-11 nipkow 2001-05-11 mult_Suc generally, not just for numerals.
2001-05-11 nipkow 2001-05-11 added mult_Suc laws to lin.arith.simpset. removed Suc n = n + #1 added earlier - #1::nat is not expected by Larry's simprocs.
2001-04-19 nipkow 2001-04-19 *** empty log message ***
2001-01-12 wenzelm 2001-01-12 HOLogic.dest_binum;
2000-12-19 paulson 2000-12-19 inserting the simproc nat_cancel_factor
2000-12-18 nipkow 2000-12-18 moved mk_bin from Numerals to HOLogic first steps towards rational lin arith
2000-12-01 nipkow 2000-12-01 Linear arithmetic now copes with mixed nat/int formulae.
2000-11-29 paulson 2000-11-29 invoking CancelNumeralFactorFun
2000-08-10 paulson 2000-08-10 new structure field "add" for CombineNumerals
2000-08-07 paulson 2000-08-07 added a dummy "thm list" argument to prove_conv for the new interface to Cancel_Numerals
2000-07-25 wenzelm 2000-07-25 rearranged setup of arithmetic procedures, avoiding global reference values;