2006-01-19 ago setup: theory -> theory;
2005-12-01 ago simprocs: static evaluation of simpset;
2005-10-21 ago Goal.prove;
2005-10-17 ago change_claset/simpset;
2005-08-01 ago simprocs: Simplifier.inherit_bounds;
2005-06-20 ago moving some generic inequalities from integer arith to nat arith
2005-06-17 ago renamed sg_ref to thy_ref;
2005-05-16 ago Use of instead of int in most numeric simprocs; avoids
2005-05-04 ago Fixing a problem with lin.arith.
2005-04-07 ago reverted renaming of Some/None in comments and strings;
2005-02-13 ago Deleted Library.option type.
2004-09-07 ago tuned "discrete" field
2004-09-06 ago made mult_mono_thms generic.
2004-07-01 ago new treatment of binary numerals
2004-05-11 ago changes made due to new Ring_and_Field theory
2004-03-19 ago New simplification ordering to move numerals together. Fixes a bug in the
2004-02-17 ago further tweaks to the numeric theories
2004-02-15 ago Polymorphic treatment of binary arithmetic using axclasses
2004-02-10 ago generic of_nat and of_int functions, and generalization of iszero
2004-01-28 ago tidying up arithmetic for the hyperreals
2004-01-28 ago converted Real/Lubs to Isar script. Converting arithmetic setup
2003-12-27 ago re-organized numeric lemmas
2003-12-25 ago re-organized some hyperreal and real lemmas
2003-12-04 ago further simplifications of the integer development; converting more .ML files
2003-12-04 ago Tidying of the integer development; towards removing the
2003-12-03 ago Simplification of the development of Integers
2003-07-15 ago Fixing a simproc bug
2002-08-13 ago Counter example generation mods.
2002-08-08 ago tuned prove_conv (error reporting done within meta_simplifier.ML);
2002-08-06 ago sane interface for simprocs;
2002-02-28 ago fixing nat_combine_numerals simprocs (again)
2001-12-12 ago new rewrite rules for use by arith_tac to take care of uminus.
2001-11-02 ago Numerals and simprocs for types real and hypreal. The abstract
2001-10-22 ago Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
2001-10-08 ago sane numerals (stage 3): provide generic "1" on all number types;
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-01-12 ago HOLogic.dest_binum;
2001-01-09 ago *** empty log message ***
2000-12-21 ago *** empty log message ***
2000-12-21 ago simproc bug fix: negative literals and large terms
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-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;