src/HOL/Arith.ML
1999-09-21 nipkow 1999-09-21 Mod because of new solver interface.
1999-09-21 nipkow 1999-09-21 ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
1999-09-01 wenzelm 1999-09-01 bind_thms;
1999-07-30 wenzelm 1999-07-30 'arith' proof method;
1999-07-30 paulson 1999-07-30 split_diff and remove_diff_ss
1999-07-27 wenzelm 1999-07-27 fixed comment;
1999-07-21 paulson 1999-07-21 a stronger diff_less and no more le_diff_less
1999-07-15 paulson 1999-07-15 qed_goal -> Goal
1999-07-13 paulson 1999-07-13 simplified the <= monotonicity proof
1999-07-10 wenzelm 1999-07-10 handle THM/TERM exn;
1999-07-01 paulson 1999-07-01 new laws mult_le_cancel1, mult_le_cancel2
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1999-03-03 paulson 1999-03-03 expandshort
1999-01-27 nipkow 1999-01-27 arith_tac for min/max
1999-01-24 nipkow 1999-01-24 Fixed a bug in lin.arith.
1999-01-14 nipkow 1999-01-14 More arith refinements.
1999-01-13 nipkow 1999-01-13 Refined arithmetic.
1999-01-13 nipkow 1999-01-13 Simplified arithmetic.
1999-01-12 nipkow 1999-01-12 Restructured Arithmatic
1999-01-11 nipkow 1999-01-11 More arith simplifications.
1999-01-09 nipkow 1999-01-09 Remoaved a few now redundant rewrite rules.
1999-01-09 nipkow 1999-01-09 Refined arith tactic.
1999-01-05 nipkow 1999-01-05 In Main: moved Bin to the left to preserve the solver in its simpset.
1999-01-04 nipkow 1999-01-04 Version 1.0 of linear nat arithmetic.
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-23 oheimb 1998-10-23 corrected auto_tac (applications of unsafe wrappers)
1998-10-16 nipkow 1998-10-16 Installed trans_tac in solver of simpset().
1998-10-02 paulson 1998-10-02 tidying
1998-10-01 nipkow 1998-10-01 a few new lemmas.
1998-09-23 paulson 1998-09-23 deleted needless parentheses
1998-09-18 paulson 1998-09-18 theorem le_diff_conv2; tidying and expandshort
1998-09-14 paulson 1998-09-14 new theorem le_diff_conv
1998-09-07 paulson 1998-09-07 tidying
1998-09-04 nipkow 1998-09-04 Arith: less_diff_conv List: [i..j]
1998-09-01 paulson 1998-09-01 changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
1998-09-01 paulson 1998-09-01 Two new subtraction lemmas
1998-08-20 paulson 1998-08-20 new theorems
1998-08-19 paulson 1998-08-19 Some new theorems. zero_less_diff replaces less_imp_diff_positive
1998-08-18 paulson 1998-08-18 new theorem diff_Suc_less_diff
1998-08-13 paulson 1998-08-13 even more tidying of Goal commands
1998-08-06 nipkow 1998-08-06 Removed duplicate thms: less_imp_add_less = trans_less_add1 le_imp_add_le = trans_le_add1
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-07-15 paulson 1998-07-15 Removal of leading "\!\!..." from most Goal commands
1998-06-25 paulson 1998-06-25 Installation of target HOL-Real
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-04-27 nipkow 1998-04-27 Added a few lemmas. Renamed expand_const -> split_const.
1998-03-12 paulson 1998-03-12 New laws, mostly generalizing old "pred" ones
1998-03-11 paulson 1998-03-11 Arith.thy -> thy; proved a few new theorems
1998-03-07 nipkow 1998-03-07 Removed `addsplits [expand_if]'
1998-03-03 paulson 1998-03-03 New theorem diff_Suc_le_Suc_diff; tidied another proof
1997-12-16 wenzelm 1997-12-16 expandshort;
1997-12-12 paulson 1997-12-12 Faster proof of mult_less_cancel2
1997-12-06 nipkow 1997-12-06 Got rid of some preds and replaced some n~=0 by 0<n.
1997-12-04 nipkow 1997-12-04 pred n -> n-1
1997-12-03 nipkow 1997-12-03 Replaced n ~= 0 by 0 < n
1997-11-26 wenzelm 1997-11-26 added Suc_mult_less_cancel1, Suc_mult_le_cancel1, Suc_mult_cancel1;
1997-11-05 paulson 1997-11-05 Expandshort; new theorem le_square
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-10-17 nipkow 1997-10-17 setloop split_tac -> addsplits