src/HOL/Library/Multiset.thy

   by (simp add: plus_multiset.rep_eq)
 
 
 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
 
 lemma count_diff [simp]: "count (M - N) a = count M a - count N a"
   by (simp add: minus_multiset.rep_eq)

   "(M::'a multiset) - N - Q = M - Q - N"
   by (auto simp add: multiset_eq_iff)
 
 lemma diff_add:
   "(M::'a multiset) - (N + Q) = M - N - Q"
+  find_theorems solves
 by (simp add: multiset_eq_iff)
 
 lemma diff_union_swap:
   "a \<noteq> b \<Longrightarrow> M - {#a#} + {#b#} = M + {#b#} - {#a#}"
   by (auto simp add: multiset_eq_iff)

 Nitpick_Model.register_term_postprocessor @{typ "'a multiset"}
     multiset_postproc
 *}
 
 end
+