src/HOL/arith_data.ML
2004-08-06 nipkow 2004-08-06 Initial changes to extend arithmetic from individual types to type classes.
2004-05-11 obua 2004-05-11 changes made due to new Ring_and_Field theory
2004-04-02 nipkow 2004-04-02 exposed fast_arith_neq_limit
2004-04-02 nipkow 2004-04-02 got rid of ignore_neq again.
2004-04-02 nipkow 2004-04-02 ignore_neq also influences arith_tac now, not just fast_arith_tac
2004-04-02 nipkow 2004-04-02 Added ignore_neq flag.
2004-01-28 paulson 2004-01-28 converted Real/Lubs to Isar script. Converting arithmetic setup files to be polymorphic.
2004-01-14 nipkow 2004-01-14 fixed old bugs in "decomp" (conversion from term to lin.arith. format). updated instantiation of real lin.arith.
2003-12-27 paulson 2003-12-27 re-organized numeric lemmas
2003-04-07 nipkow 2003-04-07 added isolate_Suc to counteract deficiencies in one of Larry's simprocs.
2003-03-25 berghofe 2003-03-25 Added hook for presburger arithmetic decision procedure.
2002-08-23 nipkow 2002-08-23 Added div+mod cancelling simproc
2002-08-13 nipkow 2002-08-13 Counter example generation mods.
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.
2002-02-25 nipkow 2002-02-25 solved the problem that Larry's simproce cancle_numerals(?) returns inconsistent inequality w/o rewriting it to False.
2001-12-12 nipkow 2001-12-12 tuned conversion from terms to "polynomials" for arith_tac: takes care of "uminus" now.
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-11-28 wenzelm 2001-11-28 theory data: removed obsolete finish method;
2001-11-08 wenzelm 2001-11-08 theory data: finish method;
2001-10-14 wenzelm 2001-10-14 improved atomize setup;
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-08-06 nipkow 2001-08-06 turned translation for 1::nat into def. introduced 1' and replaced most occurrences of 1 by 1'.
2001-05-31 nipkow 2001-05-31 Allow Suc-numerals as coefficients in lin-arith formulae
2001-01-16 wenzelm 2001-01-16 tuned atomize;
2001-01-03 paulson 2001-01-03 removal of the nat_cancel_factor simproc
2000-12-21 nipkow 2000-12-21 rational arithmetic
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-23 wenzelm 2000-11-23 arith_tac: atomize;
2000-09-07 wenzelm 2000-09-07 tuned msg;
2000-08-14 wenzelm 2000-08-14 tuned names;
2000-07-25 wenzelm 2000-07-25 rearranged setup of arithmetic procedures, avoiding global reference values;
1998-11-27 nipkow 1998-11-27 At last: linear arithmetic for nat!
1998-10-28 nipkow 1998-10-28 added nat_diff_split and a few lemmas in Trancl.
1998-10-01 paulson 1998-10-01 tidied
1998-09-24 oheimb 1998-09-24 renamed mk_meta_eq to mk_eq
1998-09-07 paulson 1998-09-07 tidying
1998-09-01 paulson 1998-09-01 Replaced Suc_diff_n by Suc_diff_le
1998-08-20 paulson 1998-08-20 adjusted for new rewrites
1998-08-13 paulson 1998-08-13 even more tidying of Goal commands
1998-08-12 oheimb 1998-08-12 renamed mk_meta_eq to meta_eq
1998-07-12 wenzelm 1998-07-12 isatool expandshort;
1998-03-03 paulson 1998-03-03 New theorem
1997-12-05 wenzelm 1997-12-05 simplification procedures nat_cancel enabled by default;
1997-12-01 wenzelm 1997-12-01 open;
1997-12-01 berghofe 1997-12-01 Added DiffCancelSums.
1997-11-27 wenzelm 1997-11-27 mk_norm_sum;
1997-11-26 wenzelm 1997-11-26 separate lists of simprocs;
1997-11-26 wenzelm 1997-11-26 Setup various arithmetic proof procedures.