changeset 20217 | 25b068a99d2b |
parent 19765 | dfe940911617 |
child 20792 | add17d26151b |
--- a/src/HOL/Hyperreal/MacLaurin.thy Wed Jul 26 13:31:07 2006 +0200 +++ b/src/HOL/Hyperreal/MacLaurin.thy Wed Jul 26 19:23:04 2006 +0200 @@ -390,7 +390,7 @@ lemma mod_exhaust_less_4: "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)" -by (case_tac "m mod 4", auto, arith) +by auto lemma Suc_Suc_mult_two_diff_two [rule_format, simp]: "0 < n --> Suc (Suc (2 * n - 2)) = 2*n"