# HG changeset patch
# User haftmann
# Date 1311629215 -7200
# Node ID 8adc47768db06070bf6aab1c6dcf500282f39687
# Parent  1fe23cfca01f13aa123437d8ba8d330f90997387
adjusted to tailored version of ball_simps

diff -r 1fe23cfca01f -r 8adc47768db0 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Jul 24 22:38:13 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Jul 25 23:26:55 2011 +0200
@@ -2539,7 +2539,7 @@
   fixes s :: "'a::real_normed_vector set"
   assumes "open s"
   shows "open(convex hull s)"
-  unfolding open_contains_cball convex_hull_explicit unfolding mem_Collect_eq ball_simps(10)
+  unfolding open_contains_cball convex_hull_explicit unfolding mem_Collect_eq ball_simps(8)
 proof(rule, rule) fix a
   assume "\<exists>sa u. finite sa \<and> sa \<subseteq> s \<and> (\<forall>x\<in>sa. 0 \<le> u x) \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = a"
   then obtain t u where obt:"finite t" "t\<subseteq>s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = a" by auto