--- a/src/HOL/MacLaurin.thy Fri Aug 19 08:40:15 2011 -0700
+++ b/src/HOL/MacLaurin.thy Fri Aug 19 10:46:54 2011 -0700
@@ -430,6 +430,7 @@
apply safe
apply (simp (no_asm))
apply (simp (no_asm) add: sin_expansion_lemma)
+apply (force intro!: DERIV_intros)
apply (subst (asm) setsum_0', clarify, case_tac "a", simp, simp)
apply (cases n, simp, simp)
apply (rule ccontr, simp)
@@ -458,6 +459,7 @@
apply safe
apply simp
apply (simp (no_asm) add: sin_expansion_lemma)
+apply (force intro!: DERIV_intros)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
@@ -474,6 +476,7 @@
apply safe
apply simp
apply (simp (no_asm) add: sin_expansion_lemma)
+apply (force intro!: DERIV_intros)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])