Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Multiset.thy
changeset 15316 2a6ff941a115
parent 15140 322485b816ac
child 15402 97204f3b4705 
--- 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
isabelle