src/HOL/Arith.ML
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
1996-02-15 nipkow 1996-02-15 Added a few thms and the new theory RelPow.
1996-02-09 nipkow 1996-02-09 Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
1996-02-05 clasohm 1996-02-05 expanded tabs; renamed subtype to typedef; incorporated Konrad's changes
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-12-08 nipkow 1995-12-08 Changed div_termination -> diff_less Corrected if_...
1995-11-12 nipkow 1995-11-12 added new arithmetic lemmas and the functions take and drop.
1995-10-25 nipkow 1995-10-25 Added various thms and tactics.
1995-10-04 clasohm 1995-10-04 added local simpsets; removed IOA from 'make test'
1995-07-26 lcp 1995-07-26 tidied proof of add_less_mono
1995-06-22 nipkow 1995-06-22 Added add_lessD1
1995-03-24 clasohm 1995-03-24 changed syntax of tuples from <..., ...> to (..., ...)
1995-03-20 clasohm 1995-03-20 changed syntax of "if"
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application