--- 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"
--- 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)"