src/HOL/Library/Multiset.thy
changeset 49388 1ffd5a055acf
parent 48040 4caf6cd063be
child 49394 52e636ace94e
     1.1 --- a/src/HOL/Library/Multiset.thy	Sat Sep 15 20:13:25 2012 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Sat Sep 15 20:14:29 2012 +0200
     1.3 @@ -122,13 +122,14 @@
     1.4  
     1.5  subsubsection {* Difference *}
     1.6  
     1.7 -instantiation multiset :: (type) minus
     1.8 +instantiation multiset :: (type) comm_monoid_diff
     1.9  begin
    1.10  
    1.11  lift_definition minus_multiset :: "'a multiset => 'a multiset => 'a multiset" is "\<lambda> M N. \<lambda>a. M a - N a"
    1.12  by (rule diff_preserves_multiset)
    1.13   
    1.14 -instance ..
    1.15 +instance
    1.16 +by default (transfer, simp add: fun_eq_iff)+
    1.17  
    1.18  end
    1.19  
    1.20 @@ -161,6 +162,7 @@
    1.21  
    1.22  lemma diff_add:
    1.23    "(M::'a multiset) - (N + Q) = M - N - Q"
    1.24 +  find_theorems solves
    1.25  by (simp add: multiset_eq_iff)
    1.26  
    1.27  lemma diff_union_swap:
    1.28 @@ -1913,3 +1915,4 @@
    1.29  *}
    1.30  
    1.31  end
    1.32 +