src/HOL/Multivariate_Analysis/Euclidean_Space.thy

--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Aug 23 11:17:13 2010 +0200
@@ -220,7 +220,7 @@
   fixes x :: "'a::real_normed_vector"
   shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
   unfolding norm_scaleR
-  apply (erule mult_mono1)
+  apply (erule mult_left_mono)
   apply simp
   done