# HG changeset patch
# User hoelzl
# Date 1450794091 -3600
# Node ID 678c3648067cb5b708fdf90c6fed9b762873551f
# Parent  ea79448eb4261cc9bfc118496ed6382366abf8c6
Weierstrass: whitespace

diff -r ea79448eb426 -r 678c3648067c src/HOL/Multivariate_Analysis/Weierstrass.thy
--- 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