author nipkow Tue, 05 Nov 2019 19:15:00 +0100 changeset 71041 fdb6c5034c24 parent 71039 ddd4aefc540f (current diff) parent 71040 9d2753406c60 (diff) child 71042 400e9512f1d3 child 71043 2fab72ab919a
merged
```--- a/src/HOL/Analysis/Convex.thy	Tue Nov 05 10:02:09 2019 -0500
+++ b/src/HOL/Analysis/Convex.thy	Tue Nov 05 19:15:00 2019 +0100
@@ -2696,8 +2696,7 @@
proof -
obtain s u where s_u: "finite s \<and> s \<noteq> {} \<and> s \<subseteq> S \<and> sum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = 0"
using assms affine_hull_explicit[of S] by auto
-  then have "\<exists>v\<in>s. u v \<noteq> 0"
-    using sum_not_0[of "u" "s"] by auto
+  then have "\<exists>v\<in>s. u v \<noteq> 0" by auto
then have "finite s \<and> s \<subseteq> S \<and> (\<exists>v\<in>s. u v \<noteq> 0 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = 0)"
using s_u by auto
then show ?thesis
@@ -3483,7 +3482,7 @@
have "sum c s = 0"
moreover have "\<not> (\<forall>v\<in>s. c v = 0)"
-      by (metis (no_types) IntD1 \<open>s \<inter> t = t\<close> a1 c_def sum_not_0 zero_neq_one)
+      by (metis (no_types) IntD1 \<open>s \<inter> t = t\<close> a1 c_def sum.neutral zero_neq_one)
moreover have "(\<Sum>v\<in>s. c v *\<^sub>R v) = 0"
by (simp add: c_def if_smult sum_negf
```--- a/src/HOL/Analysis/Linear_Algebra.thy	Tue Nov 05 10:02:09 2019 -0500