# HG changeset patch
# User nipkow
# Date 1572977700 -3600
# Node ID fdb6c5034c24c7d367ff718e15369c702eb5ddbd
# Parent  ddd4aefc540f9f121c807711198014d089d199d9# Parent  9d2753406c605002d06a0d1c565eb3fe6bb74b7a
merged

diff -r ddd4aefc540f -r fdb6c5034c24 src/HOL/Analysis/Convex.thy
--- 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"
       by (simp add: c_def comm_monoid_add_class.sum.If_cases \<open>finite s\<close> sum_negf)
     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
              comm_monoid_add_class.sum.If_cases \<open>finite s\<close>)
diff -r ddd4aefc540f -r fdb6c5034c24 src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Tue Nov 05 10:02:09 2019 -0500
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Tue Nov 05 19:15:00 2019 +0100
@@ -50,9 +50,6 @@
 lemma independent_substdbasis: "d \<subseteq> Basis \<Longrightarrow> independent d"
   by (rule independent_mono[OF independent_Basis])
 
-lemma sum_not_0: "sum f A \<noteq> 0 \<Longrightarrow> \<exists>a \<in> A. f a \<noteq> 0"
-  by (rule ccontr) auto
-
 lemma subset_translation_eq [simp]:
     fixes a :: "'a::real_vector" shows "(+) a ` s \<subseteq> (+) a ` t \<longleftrightarrow> s \<subseteq> t"
   by auto