src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy

     unfolding is_interval_convex_1 [symmetric] is_interval_def Basis_real_def
     by - (clarify, simp (no_asm_use), fast)
 qed
 
 lemma unit_interval_convex_hull:
-  defines "One \<equiv> \<Sum>Basis"
-  shows "cbox (0::'a::euclidean_space) One = convex hull {x. \<forall>i\<in>Basis. (x\<bullet>i = 0) \<or> (x\<bullet>i = 1)}"
+  "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)
   have "?int = {x. \<forall>i\<in>Basis. x \<bullet> i \<in> cbox 0 1}"