--- a/src/HOL/Transcendental.thy Thu Aug 18 18:10:23 2011 -0700
+++ b/src/HOL/Transcendental.thy Thu Aug 18 19:53:03 2011 -0700
@@ -881,7 +881,7 @@
by (simp add: diffs_def)
lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
-by (auto intro!: ext simp add: exp_def)
+by (auto simp add: exp_def)
lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)"
apply (simp add: exp_def)
@@ -1248,7 +1248,7 @@
by (rule DERIV_diff)
thus "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> 0" by auto
qed (auto simp add: assms)
- thus ?thesis by (auto simp add: suminf_zero)
+ thus ?thesis by auto
qed
subsection {* Sine and Cosine *}
@@ -1337,10 +1337,10 @@
by (auto intro!: sums_unique sums_minus sin_converges)
lemma lemma_sin_ext: "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
-by (auto intro!: ext simp add: sin_def)
+ by (auto simp add: sin_def)
lemma lemma_cos_ext: "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
-by (auto intro!: ext simp add: cos_def)
+ by (auto simp add: cos_def)
lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
apply (simp add: cos_def)