--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Jan 06 16:17:50 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Jan 07 13:42:43 2016 +0100
@@ -5978,7 +5978,7 @@
(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)"