src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy

 lemma unit_interval_convex_hull:
   "cbox (0::'a::euclidean_space) One = convex hull {x. \<forall>i\<in>Basis. (x\<bullet>i = 0) \<or> (x\<bullet>i = 1)}"
   (is "?int = convex hull ?points")
 proof -
   have One[simp]: "\<And>i. i \<in> Basis \<Longrightarrow> One \<bullet> i = 1"
-    by (simp add: One_def inner_setsum_left setsum.If_cases inner_Basis)
+    by (simp add: inner_setsum_left setsum.If_cases inner_Basis)
   have "?int = {x. \<forall>i\<in>Basis. x \<bullet> i \<in> cbox 0 1}"
     by (auto simp: cbox_def)
   also have "\<dots> = (\<Sum>i\<in>Basis. (\<lambda>x. x *\<^sub>R i) ` cbox 0 1)"
     by (simp only: box_eq_set_setsum_Basis)
   also have "\<dots> = (\<Sum>i\<in>Basis. (\<lambda>x. x *\<^sub>R i) ` (convex hull {0, 1}))"