--- a/src/HOL/Library/Multiset.thy Sat Sep 15 20:13:25 2012 +0200
+++ b/src/HOL/Library/Multiset.thy Sat Sep 15 20:14:29 2012 +0200
@@ -122,13 +122,14 @@
subsubsection {* Difference *}
-instantiation multiset :: (type) minus
+instantiation multiset :: (type) comm_monoid_diff
begin
lift_definition minus_multiset :: "'a multiset => 'a multiset => 'a multiset" is "\<lambda> M N. \<lambda>a. M a - N a"
by (rule diff_preserves_multiset)
-instance ..
+instance
+by default (transfer, simp add: fun_eq_iff)+
end
@@ -161,6 +162,7 @@
lemma diff_add:
"(M::'a multiset) - (N + Q) = M - N - Q"
+ find_theorems solves
by (simp add: multiset_eq_iff)
lemma diff_union_swap:
@@ -1913,3 +1915,4 @@
*}
end
+