src/HOL/Hyperreal/MacLaurin.thy
changeset 15251 bb6f072c8d10
parent 15234 ec91a90c604e
child 15481 fc075ae929e4
     1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Mon Oct 18 13:40:45 2004 +0200
     1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Tue Oct 19 18:18:45 2004 +0200
     1.3 @@ -10,10 +10,10 @@
     1.4  begin
     1.5  
     1.6  lemma sumr_offset: "sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f"
     1.7 -by (induct_tac "n", auto)
     1.8 +by (induct "n", auto)
     1.9  
    1.10  lemma sumr_offset2: "\<forall>f. sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f"
    1.11 -by (induct_tac "n", auto)
    1.12 +by (induct "n", auto)
    1.13  
    1.14  lemma sumr_offset3: "sumr 0 (n+k) f = sumr 0 n (%m. f (m+k)) + sumr 0 k f"
    1.15  by (simp  add: sumr_offset)
    1.16 @@ -292,7 +292,7 @@
    1.17         diff 0 0 =
    1.18         (\<Sum>m = 0..<n. diff m 0 * 0 ^ m / real (fact m)) +
    1.19         diff n 0 * 0 ^ n / real (fact n)"
    1.20 -by (induct_tac "n", auto)
    1.21 +by (induct "n", auto)
    1.22  
    1.23  lemma Maclaurin_bi_le:
    1.24     "[| diff 0 = f;
    1.25 @@ -405,15 +405,15 @@
    1.26  
    1.27  lemma Suc_Suc_mult_two_diff_two [rule_format, simp]:
    1.28       "0 < n --> Suc (Suc (2 * n - 2)) = 2*n"
    1.29 -by (induct_tac "n", auto)
    1.30 +by (induct "n", auto)
    1.31  
    1.32  lemma lemma_Suc_Suc_4n_diff_2 [rule_format, simp]:
    1.33       "0 < n --> Suc (Suc (4*n - 2)) = 4*n"
    1.34 -by (induct_tac "n", auto)
    1.35 +by (induct "n", auto)
    1.36  
    1.37  lemma Suc_mult_two_diff_one [rule_format, simp]:
    1.38        "0 < n --> Suc (2 * n - 1) = 2*n"
    1.39 -by (induct_tac "n", auto)
    1.40 +by (induct "n", auto)
    1.41  
    1.42  
    1.43  text{*It is unclear why so many variant results are needed.*}
    1.44 @@ -496,7 +496,7 @@
    1.45                 then (- 1) ^ (m div 2)/(real  (fact m))
    1.46                 else 0) *
    1.47                0 ^ m) = 1"
    1.48 -by (induct_tac "n", auto)
    1.49 +by (induct "n", auto)
    1.50  
    1.51  lemma Maclaurin_cos_expansion:
    1.52       "\<exists>t. abs t \<le> abs x &