# HG changeset patch
# User nipkow
# Date 1550047816 -3600
# Node ID 6ec272e153f0fab0331adb75dabe85c91394fb05
# Parent  a99a0f5474c5fa95b40e9e6867b148493e09b838
removed subsumed lemma

diff -r a99a0f5474c5 -r 6ec272e153f0 src/HOL/Analysis/Convex.thy
--- a/src/HOL/Analysis/Convex.thy	Wed Feb 13 07:48:42 2019 +0100
+++ b/src/HOL/Analysis/Convex.thy	Wed Feb 13 09:50:16 2019 +0100
@@ -1203,7 +1203,7 @@
         have c: "card (S - {x}) = card S - 1"
           by (simp add: Suc.prems(3) \<open>x \<in> S\<close>)
         have "sum u (S - {x}) = 1 - u x"
-          by (simp add: Suc.prems sum_diff1_ring \<open>x \<in> S\<close>)
+          by (simp add: Suc.prems sum_diff1 \<open>x \<in> S\<close>)
         with x have eq1: "inverse (1 - u x) * sum u (S - {x}) = 1"
           by auto
         have inV: "(\<Sum>y\<in>S - {x}. (inverse (1 - u x) * u y) *\<^sub>R y) \<in> V"
diff -r a99a0f5474c5 -r 6ec272e153f0 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Wed Feb 13 07:48:42 2019 +0100
+++ b/src/HOL/Groups_Big.thy	Wed Feb 13 09:50:16 2019 +0100
@@ -848,12 +848,6 @@
   finally show ?case .
 qed
 
-lemma sum_diff1_ring:
-  fixes f :: "'b \<Rightarrow> 'a::ring"
-  assumes "finite A" "a \<in> A"
-  shows "sum f (A - {a}) = sum f A - (f a)"
-  unfolding sum.remove [OF assms] by auto
-
 lemma sum_product:
   fixes f :: "'a \<Rightarrow> 'b::semiring_0"
   shows "sum f A * sum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"