--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Apr 09 09:37:47 2014 +0200
@@ -2277,7 +2277,9 @@
using Min_ge_iff[of i 0 ] and obt(1)
unfolding t_def i_def
using obt(4)[unfolded le_less]
- apply (auto simp: divide_le_0_iff divide_minus_right)
+ apply auto
+ unfolding divide_le_0_iff
+ apply auto
done
have t: "\<forall>v\<in>s. u v + t * w v \<ge> 0"
proof
@@ -2314,7 +2316,7 @@
obtain a where "a \<in> s" and "t = (\<lambda>v. (u v) / (- w v)) a" and "w a < 0"
using Min_in[OF _ `i\<noteq>{}`] and obt(1) unfolding i_def t_def by auto
- then have a: "a \<in> s" "u a + t * w a = 0" by (auto simp: divide_minus_right)
+ then have a: "a \<in> s" "u a + t * w a = 0" by auto
have *: "\<And>f. setsum f (s - {a}) = setsum f s - ((f a)::'b::ab_group_add)"
unfolding setsum_diff1'[OF obt(1) `a\<in>s`] by auto
have "(\<Sum>v\<in>s. u v + t * w v) = 1"