src/HOL/Transcendental.thy
changeset 44289 d81d09cdab9c
parent 44282 f0de18b62d63
child 44305 3bdc02eb1637
     1.1 --- a/src/HOL/Transcendental.thy	Thu Aug 18 18:10:23 2011 -0700
     1.2 +++ b/src/HOL/Transcendental.thy	Thu Aug 18 19:53:03 2011 -0700
     1.3 @@ -881,7 +881,7 @@
     1.4  by (simp add: diffs_def)
     1.5  
     1.6  lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
     1.7 -by (auto intro!: ext simp add: exp_def)
     1.8 +by (auto simp add: exp_def)
     1.9  
    1.10  lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)"
    1.11  apply (simp add: exp_def)
    1.12 @@ -1248,7 +1248,7 @@
    1.13        by (rule DERIV_diff)
    1.14      thus "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> 0" by auto
    1.15    qed (auto simp add: assms)
    1.16 -  thus ?thesis by (auto simp add: suminf_zero)
    1.17 +  thus ?thesis by auto
    1.18  qed
    1.19  
    1.20  subsection {* Sine and Cosine *}
    1.21 @@ -1337,10 +1337,10 @@
    1.22  by (auto intro!: sums_unique sums_minus sin_converges)
    1.23  
    1.24  lemma lemma_sin_ext: "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
    1.25 -by (auto intro!: ext simp add: sin_def)
    1.26 +  by (auto simp add: sin_def)
    1.27  
    1.28  lemma lemma_cos_ext: "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
    1.29 -by (auto intro!: ext simp add: cos_def)
    1.30 +  by (auto simp add: cos_def)
    1.31  
    1.32  lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
    1.33  apply (simp add: cos_def)