--- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Wed Jan 13 23:07:06 2016 +0100
@@ -272,7 +272,7 @@
qed
qed
-text{*Alternative version, formulated as in HOL Light*}
+text\<open>Alternative version, formulated as in HOL Light\<close>
corollary series_comparison_uniform:
fixes f :: "_ \<Rightarrow> nat \<Rightarrow> _ :: banach"
assumes g: "summable g" and le: "\<And>n x. N \<le> n \<and> x \<in> A \<Longrightarrow> norm(f x n) \<le> g n"