src/HOL/Hoare/Arith2.ML
2004-01-12 paulson 2004-01-12 Added lemmas to Ring_and_Field with slightly modified simplification rules Deleted some little-used integer theorems, replacing them by the generic ones in Ring_and_Field Consolidated integer powers
2001-10-06 wenzelm 2001-10-06 * sane numerals (stage 2): plain "num" syntax (removed "#");
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2000-09-15 paulson 2000-09-15 renamed (most of...) the select rules
2000-05-04 paulson 2000-05-04 changed 2 to #2
1999-09-07 wenzelm 1999-09-07 isatool expandshort;
1999-07-29 paulson 1999-07-29 added parentheses to cope with a possible reduction of the precedence of unary minus
1998-07-03 nipkow 1998-07-03 Removed leading !! in goals.
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1997-12-04 nipkow 1997-12-04 Simplified proofs.
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-05-30 paulson 1997-05-30 Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
1997-05-26 paulson 1997-05-26 Renamed lessD to Suc_leI
1997-05-20 paulson 1997-05-20 Some theorems moved to HOL/Arith.ML
1997-04-24 nipkow 1997-04-24 Introduced a generic "induct_tac" which picks up the right induction scheme automatically. Also changed nat_ind_tac, which does no longer append a "1" to the name of the induction variable. This caused some changes...
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-07-19 berghofe 1996-07-19 Classical tactics now use default claset.
1996-05-01 paulson 1996-05-01 Deleted diff_mult_distrib_r as diff_mult_distrib is not proved in Arith.
1996-02-05 clasohm 1996-02-05 expanded tabs; incorporated Konrad's changes
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-11-17 nipkow 1995-11-17 New directory. Hoare logic according to Mike Gordon.