src/HOL/MacLaurin.thy
changeset 57492 74bf65a1910a
parent 57418 6ab1c7cb0b8d
child 57514 bdc2c6b40bf2
     1.1 --- a/src/HOL/MacLaurin.thy	Wed Jul 02 17:34:45 2014 +0200
     1.2 +++ b/src/HOL/MacLaurin.thy	Wed Jun 11 14:24:23 2014 +1000
     1.3 @@ -419,8 +419,7 @@
     1.4  apply (simp (no_asm))
     1.5  apply (simp (no_asm) add: sin_expansion_lemma)
     1.6  apply (force intro!: derivative_eq_intros)
     1.7 -apply (subst (asm) setsum.neutral, clarify, case_tac "x", simp, simp)
     1.8 -apply (cases n, simp, simp)
     1.9 +apply (subst (asm) setsum.neutral, auto)[1]
    1.10  apply (rule ccontr, simp)
    1.11  apply (drule_tac x = x in spec, simp)
    1.12  apply (erule ssubst)