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