src/HOL/MacLaurin.thy
changeset 51489 f738e6dbd844
parent 49962 a8cc904a6820
child 56181 2aa0b19e74f3
     1.1 --- a/src/HOL/MacLaurin.thy	Sat Mar 23 17:11:06 2013 +0100
     1.2 +++ b/src/HOL/MacLaurin.thy	Sat Mar 23 20:50:39 2013 +0100
     1.3 @@ -428,7 +428,7 @@
     1.4  apply (simp (no_asm))
     1.5  apply (simp (no_asm) add: sin_expansion_lemma)
     1.6  apply (force intro!: DERIV_intros)
     1.7 -apply (subst (asm) setsum_0', clarify, case_tac "a", simp, simp)
     1.8 +apply (subst (asm) setsum_0', clarify, case_tac "x", simp, simp)
     1.9  apply (cases n, simp, simp)
    1.10  apply (rule ccontr, simp)
    1.11  apply (drule_tac x = x in spec, simp)