--- a/src/HOL/Library/Multiset.thy Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/Library/Multiset.thy Mon Mar 23 19:05:14 2015 +0100
@@ -95,8 +95,11 @@
lift_definition plus_multiset :: "'a multiset => 'a multiset => 'a multiset" is "\<lambda>M N. (\<lambda>a. M a + N a)"
by (rule union_preserves_multiset)
+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
-by default (transfer, simp add: fun_eq_iff)+
+ by default (transfer, simp add: fun_eq_iff)+
end
@@ -129,9 +132,6 @@
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
by default (transfer, simp add: fun_eq_iff)+