--- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Tue Mar 31 15:01:06 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Tue Mar 31 16:48:48 2015 +0100
@@ -407,7 +407,7 @@
hence "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2)
\<le> (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)"
by (auto intro!: setsum_mono
- simp add: clamp_def dist_real_def real_abs_le_square_iff[symmetric])
+ simp add: clamp_def dist_real_def abs_le_square_iff[symmetric])
thus ?thesis
by (auto intro: real_sqrt_le_mono
simp add: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def)