src/HOL/Arith.ML
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
1997-10-16 paulson 1997-10-16 New simprule diff_le_self, requiring a new proof of diff_diff_cancel
1997-10-16 nipkow 1997-10-16 Various new lemmas. Improved conversion of equations to rewrite rules: (s=t becomes (s=t)==True if s=t loops).
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-09-29 paulson 1997-09-29 Step_tac -> Safe_tac
1997-09-26 paulson 1997-09-26 Minor tidying to use Clarify_tac, etc.
1997-07-02 nipkow 1997-07-02 Added the following lemmas tp Divides and a few others to Arith and NatDef: div_le_mono, div_le_mono2, div_le_dividend, div_less_dividend Fixed a broken proof in WF_Rel.ML. No idea what caused this.
1997-06-23 paulson 1997-06-23 Ran expandshort
1997-06-04 wenzelm 1997-06-04 eliminated non-ASCII;
1997-06-02 paulson 1997-06-02 New theorems le_add_diff_inverse, le_add_diff_inverse2
1997-05-30 paulson 1997-05-30 Moving div and mod from Arith to Divides Moving dvd from ex/Primes to Divides
1997-05-27 paulson 1997-05-27 New theorems suggested by Florian Kammueller
1997-05-26 paulson 1997-05-26 Tidying and a couple of useful lemmas
1997-05-22 paulson 1997-05-22 New lemmas used for ex/Fib
1997-05-20 paulson 1997-05-20 New theorems from Hoare/Arith2.ML
1997-04-09 paulson 1997-04-09 Using Blast_tac
1997-02-25 pusch 1997-02-25 minor changes due to new primrec definitions for +,-,*
1997-01-09 paulson 1997-01-09 New theorem add_leE
1996-10-16 nipkow 1996-10-16 Defined pred using nat_case rather than nat_rec. Added expand_nat_case
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-09-23 paulson 1996-09-23 Proof of mult_le_mono is now more robust
1996-09-12 paulson 1996-09-12 Change to best_tac required to prevent looping
1996-08-19 paulson 1996-08-19 Removal of less_SucE as default SE rule
1996-06-14 paulson 1996-06-14 New lemmas for gcd example
1996-06-03 berghofe 1996-06-03 best_tac, deepen_tac and safe_tac now also use default claset.
1996-05-24 berghofe 1996-05-24 Rules pred_0, pred_Suc etc. are now stored in theorem database.
1996-05-23 berghofe 1996-05-23 Replaced fast_tac by Fast_tac (which uses default claset) New rules are now also added to default claset.
1996-05-01 paulson 1996-05-01 New cancellation and monotonicity laws, about multiplication and division, from ZF/Arith.
1996-04-17 oheimb 1996-04-17 *** empty log message ***
1996-04-11 nipkow 1996-04-11 Added a number of lemmas
1996-03-28 paulson 1996-03-28 Moved even/odd lemmas from ex/Mutil to Arith
1996-03-27 paulson 1996-03-27 Library changes for mutilated checkerboard
1996-03-06 paulson 1996-03-06 Ran expandshort