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