src/HOL/Integ/int_arith1.ML
2004-09-07 nipkow 2004-09-07 tuned "discrete" field
2004-09-06 nipkow 2004-09-06 made mult_mono_thms generic.
2004-07-01 paulson 2004-07-01 new treatment of binary numerals
2004-05-11 obua 2004-05-11 changes made due to new Ring_and_Field theory
2004-03-19 paulson 2004-03-19 New simplification ordering to move numerals together. Fixes a bug in the nat cancellation simprocs
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
2004-01-28 paulson 2004-01-28 tidying up arithmetic for the hyperreals
2004-01-28 paulson 2004-01-28 converted Real/Lubs to Isar script. Converting arithmetic setup files to be polymorphic.
2003-12-27 paulson 2003-12-27 re-organized numeric lemmas
2003-12-25 paulson 2003-12-25 re-organized some hyperreal and real lemmas
2003-12-04 paulson 2003-12-04 further simplifications of the integer development; converting more .ML files to Isar scripts
2003-12-04 paulson 2003-12-04 Tidying of the integer development; towards removing the abel_cancel simproc
2003-12-03 paulson 2003-12-03 Simplification of the development of Integers
2003-07-15 paulson 2003-07-15 Fixing a simproc bug
2002-08-13 nipkow 2002-08-13 Counter example generation mods.
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-28 paulson 2002-02-28 fixing nat_combine_numerals simprocs (again) Theorem eq_cong2 moved from Integ/int_arith1.ML to simpdata.ML, where it will be available in all theories. Function simplify_meta_eq now makes the meta-equality first so that eq_cong2 will work properly.
2001-12-12 nipkow 2001-12-12 new rewrite rules for use by arith_tac to take care of uminus.
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-08 wenzelm 2001-10-08 sane numerals (stage 3): provide generic "1" on all number types;
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-01-12 wenzelm 2001-01-12 HOLogic.dest_binum;
2001-01-09 nipkow 2001-01-09 *** empty log message ***
2000-12-21 nipkow 2000-12-21 *** empty log message ***
2000-12-21 paulson 2000-12-21 simproc bug fix: negative literals and large terms
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-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;