src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
 changeset 56479 91958d4b30f7 parent 56409 36489d77c484 child 56480 093ea91498e6
```     1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Apr 08 23:16:00 2014 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Apr 09 09:37:47 2014 +0200
1.3 @@ -2277,7 +2277,9 @@
1.4        using Min_ge_iff[of i 0 ] and obt(1)
1.5        unfolding t_def i_def
1.6        using obt(4)[unfolded le_less]
1.7 -      apply (auto simp: divide_le_0_iff divide_minus_right)
1.8 +      apply auto
1.9 +      unfolding divide_le_0_iff
1.10 +      apply auto
1.11        done
1.12      have t: "\<forall>v\<in>s. u v + t * w v \<ge> 0"
1.13      proof
1.14 @@ -2314,7 +2316,7 @@
1.15
1.16      obtain a where "a \<in> s" and "t = (\<lambda>v. (u v) / (- w v)) a" and "w a < 0"
1.17        using Min_in[OF _ `i\<noteq>{}`] and obt(1) unfolding i_def t_def by auto
1.18 -    then have a: "a \<in> s" "u a + t * w a = 0" by (auto simp: divide_minus_right)
1.19 +    then have a: "a \<in> s" "u a + t * w a = 0" by auto
1.20      have *: "\<And>f. setsum f (s - {a}) = setsum f s - ((f a)::'b::ab_group_add)"
1.21        unfolding setsum_diff1'[OF obt(1) `a\<in>s`] by auto
1.22      have "(\<Sum>v\<in>s. u v + t * w v) = 1"
```