# HG changeset patch
# User nipkow
# Date 1101224583 -3600
# Node ID 2a6ff941a1159f39c4e4f2024feb11cf3790f5e9
# Parent  a358e31572d943bb236cb4c520e0b3c45d68cb50
renamed 1 lemmas

diff -r a358e31572d9 -r 2a6ff941a115 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Nov 23 16:42:54 2004 +0100
+++ b/src/HOL/Library/Multiset.thy	Tue Nov 23 16:43:03 2004 +0100
@@ -309,7 +309,7 @@
     apply (subgoal_tac "{x. x \<noteq> a \<and> 0 < f x} = {x. 0 < f x} - {a}")
      prefer 2
      apply blast
-    apply (simp add: le_imp_diff_is_add setsum_diff1 cong: conj_cong)
+    apply (simp add: le_imp_diff_is_add setsum_diff1_nat cong: conj_cong)
     done
 qed