src/HOL/arith_data.ML
2006-01-19 ago setup: theory -> theory;
2005-12-13 ago simpset for computation in raw_arith_tac added just as comment, nothing changed!
2005-12-01 ago simprocs: static evaluation of simpset;
2005-10-25 ago EVERY;
2005-10-25 ago avoid legacy goals;
2005-10-21 ago OldGoals;
2005-10-21 ago introduced functions from Pure/General/rat.ML
2005-10-17 ago change_claset/simpset;
2005-09-23 ago Provers/Arith/fast_lin_arith.ML: Simplifier.inherit_bounds;
2005-09-12 ago introduced new-style AList operations
2005-08-01 ago tuned msg;
2005-07-14 ago HOL.Not;
2005-07-07 ago linear arithmetic now takes "&" in assumptions apart.
2005-06-20 ago get_thm instead of obsolete Goals.get_thm;
2005-06-20 ago moving some generic inequalities from integer arith to nat arith
2005-06-17 ago accomodate change of TheoryDataFun;
2005-06-10 ago IntInf change
2005-05-16 ago Use of IntInf.int instead of int in most numeric simprocs; avoids
2005-05-13 ago -(n::nat) is now regarded as atomic
2005-05-04 ago fixed lin.arith
2005-05-04 ago Fixing a problem with lin.arith.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-10-07 ago simplification tweaks for better arithmetic reasoning
2004-10-01 ago tweaking of arithmetic proofs
2004-09-10 ago Added antisymmetry simproc
2004-09-10 ago new forward deduction capability for simplifier
2004-09-07 ago tuned "discrete" field
2004-09-06 ago made mult_mono_thms generic.
2004-08-06 ago Initial changes to extend arithmetic from individual types to type classes.
2004-05-11 ago changes made due to new Ring_and_Field theory
2004-04-02 ago exposed fast_arith_neq_limit
2004-04-02 ago got rid of ignore_neq again.
2004-04-02 ago ignore_neq also influences arith_tac now, not just fast_arith_tac
2004-04-02 ago Added ignore_neq flag.
2004-01-28 ago converted Real/Lubs to Isar script. Converting arithmetic setup
2004-01-14 ago fixed old bugs in "decomp" (conversion from term to lin.arith. format).
2003-12-27 ago re-organized numeric lemmas
2003-04-07 ago added isolate_Suc to counteract deficiencies in one of Larry's simprocs.
2003-03-25 ago Added hook for presburger arithmetic decision procedure.
2002-08-23 ago Added div+mod cancelling simproc
2002-08-13 ago Counter example generation mods.
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
2002-02-25 ago solved the problem that Larry's simproce cancle_numerals(?) returns
2001-12-12 ago tuned conversion from terms to "polynomials" for arith_tac: takes care
2001-12-01 ago renamed class "term" to "type" (actually "HOL.type");
2001-11-28 ago theory data: removed obsolete finish method;
2001-11-08 ago theory data: finish method;
2001-10-14 ago improved atomize setup;
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-08-06 ago turned translation for 1::nat into def.
2001-05-31 ago Allow Suc-numerals as coefficients in lin-arith formulae
2001-01-16 ago tuned atomize;
2001-01-03 ago removal of the nat_cancel_factor simproc
2000-12-21 ago rational arithmetic
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-23 ago arith_tac: atomize;