--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sat Mar 24 16:27:04 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sun Mar 25 20:15:39 2012 +0200
@@ -281,7 +281,7 @@
lemma scaleR_2:
fixes x :: "'a::real_vector"
shows "scaleR 2 x = x + x"
-unfolding one_add_one_is_two [symmetric] scaleR_left_distrib by simp
+unfolding one_add_one [symmetric] scaleR_left_distrib by simp
lemma vector_choose_size: "0 <= c ==> \<exists>(x::'a::euclidean_space). norm x = c"
apply (rule exI[where x="c *\<^sub>R basis 0 ::'a"]) using DIM_positive[where 'a='a] by auto