--- a/src/HOL/Multivariate_Analysis/Weierstrass.thy Tue Dec 22 14:31:39 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Weierstrass.thy Tue Dec 22 15:21:31 2015 +0100
@@ -203,7 +203,7 @@
apply (rule cSUP_upper, assumption)
by (simp add: bounded_imp_bdd_above compact compact_continuous_image compact_imp_bounded continuous_on_rabs)
-lemma normf_least: "s \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> s \<Longrightarrow> \<bar>f x\<bar> \<le> M) \<Longrightarrow> normf f \<le> M"
+ lemma normf_least: "s \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> s \<Longrightarrow> \<bar>f x\<bar> \<le> M) \<Longrightarrow> normf f \<le> M"
by (simp add: normf_def cSUP_least)
end