1.1 --- a/src/HOL/MacLaurin.thy	Fri Aug 19 08:40:15 2011 -0700
     1.2 +++ b/src/HOL/MacLaurin.thy	Fri Aug 19 10:46:54 2011 -0700
     1.3 @@ -430,6 +430,7 @@
     1.4  apply safe
     1.5  apply (simp (no_asm))
     1.6  apply (simp (no_asm) add: sin_expansion_lemma)
     1.7 +apply (force intro!: DERIV_intros)
     1.8  apply (subst (asm) setsum_0', clarify, case_tac "a", simp, simp)
     1.9  apply (cases n, simp, simp)
    1.10  apply (rule ccontr, simp)
    1.11 @@ -458,6 +459,7 @@
    1.12  apply safe
    1.13  apply simp
    1.14  apply (simp (no_asm) add: sin_expansion_lemma)
    1.15 +apply (force intro!: DERIV_intros)
    1.16  apply (erule ssubst)
    1.17  apply (rule_tac x = t in exI, simp)
    1.18  apply (rule setsum_cong[OF refl])
    1.19 @@ -474,6 +476,7 @@
    1.20  apply safe
    1.21  apply simp
    1.22  apply (simp (no_asm) add: sin_expansion_lemma)
    1.23 +apply (force intro!: DERIV_intros)
    1.24  apply (erule ssubst)
    1.25  apply (rule_tac x = t in exI, simp)
    1.26  apply (rule setsum_cong[OF refl])