src/HOL/arith_data.ML
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.