Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
renamed 1 lemmas
authornipkow
Tue, 23 Nov 2004 16:43:03 +0100
changeset 15316 2a6ff941a115
parent 15315 a358e31572d9
child 15317 ebdd193e15ec
renamed 1 lemmas
src/HOL/Library/Multiset.thy file | annotate | diff | comparison | revisions 
--- 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