# HG changeset patch
# User wenzelm
# Date 1452170563 -3600
# Node ID c4d6066332408dc2303b34084d4fb26b8f145b32
# Parent  969119292e25360defb6e70e14f0fba1d246ff72
tuned;

diff -r 969119292e25 -r c4d606633240 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- 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)"