diff -r 4e6e850e97c2 -r bf3d9f113474 src/HOL/Multivariate_Analysis/Summation.thy
--- a/src/HOL/Multivariate_Analysis/Summation.thy	Tue Jan 05 21:55:40 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Summation.thy	Tue Jan 05 21:57:21 2016 +0100
@@ -141,7 +141,7 @@
   with l obtain l' where l': "l = ereal l'" by (cases l) simp_all
 
   def c \<equiv> "(1 - l') / 2"
-  from l and `l \<ge> 0` have c: "l + c > l" "l' + c \<ge> 0" "l' + c < 1" unfolding c_def 
+  from l and \<open>l \<ge> 0\<close> have c: "l + c > l" "l' + c \<ge> 0" "l' + c < 1" unfolding c_def 
     by (simp_all add: field_simps l')
   have "\<forall>C>l. eventually (\<lambda>n. ereal (root n (norm (f n))) < C) sequentially"
     by (subst Limsup_le_iff[symmetric]) (simp add: l_def)