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.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.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)"