# HG changeset patch
# User hoelzl
# Date 1428847493 -7200
# Node ID 4b77fc0b3514416db52d15f56df3ad7f7e149911
# Parent  d84b355f341fa52c9e76316a5bf65a9683fb17fe
fix latex in Transcendental

diff -r d84b355f341f -r 4b77fc0b3514 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Apr 12 00:26:24 2015 +0200
+++ b/src/HOL/Transcendental.thy	Sun Apr 12 16:04:53 2015 +0200
@@ -5201,7 +5201,7 @@
   then have wnz: "\<And>w. w \<noteq> 0 \<Longrightarrow> (\<Sum>i\<le>n. c (Suc i) * w^i) = 0"
     using Suc  by auto
   then have "(\<lambda>h. \<Sum>i\<le>n. c (Suc i) * h^i) -- 0 --> 0"
-    by (simp cong: LIM_cong)                   --{*the case @{term"w=0"} by continuity}*}
+    by (simp cong: LIM_cong)                   --{*the case @{term"w=0"} by continuity*}
   then have "(\<Sum>i\<le>n. c (Suc i) * 0^i) = 0"
     using isCont_polynom [of 0 "\<lambda>i. c (Suc i)" n] LIM_unique
     by (force simp add: Limits.isCont_iff)