src/HOL/Transcendental.thy
changeset 60035 4b77fc0b3514
parent 60020 065ecea354d0
child 60036 218fcc645d22
     1.1 --- a/src/HOL/Transcendental.thy	Sun Apr 12 00:26:24 2015 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Sun Apr 12 16:04:53 2015 +0200
     1.3 @@ -5201,7 +5201,7 @@
     1.4    then have wnz: "\<And>w. w \<noteq> 0 \<Longrightarrow> (\<Sum>i\<le>n. c (Suc i) * w^i) = 0"
     1.5      using Suc  by auto
     1.6    then have "(\<lambda>h. \<Sum>i\<le>n. c (Suc i) * h^i) -- 0 --> 0"
     1.7 -    by (simp cong: LIM_cong)                   --{*the case @{term"w=0"} by continuity}*}
     1.8 +    by (simp cong: LIM_cong)                   --{*the case @{term"w=0"} by continuity*}
     1.9    then have "(\<Sum>i\<le>n. c (Suc i) * 0^i) = 0"
    1.10      using isCont_polynom [of 0 "\<lambda>i. c (Suc i)" n] LIM_unique
    1.11      by (force simp add: Limits.isCont_iff)