# HG changeset patch
# User huffman
# Date 1338278911 -7200
# Node ID 846ff14337a42b1f6d6161ed88f22fd132b6e8d0
# Parent  955ea323ddcc4260a5ecce696bc3333b723ae11a
use transfer method for instance proof

diff -r 955ea323ddcc -r 846ff14337a4 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon May 28 20:51:23 2012 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue May 29 10:08:31 2012 +0200
@@ -79,7 +79,7 @@
 
 text {* Multiset enumeration *}
 
-instantiation multiset :: (type) "{zero, plus}"
+instantiation multiset :: (type) cancel_comm_monoid_add
 begin
 
 lift_definition zero_multiset :: "'a multiset" is "\<lambda>a. 0"
@@ -91,7 +91,8 @@
 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)
 
-instance ..
+instance
+by default (transfer, simp add: fun_eq_iff)+
 
 end
 
@@ -118,9 +119,6 @@
 lemma count_union [simp]: "count (M + N) a = count M a + count N a"
   by (simp add: plus_multiset.rep_eq)
 
-instance multiset :: (type) cancel_comm_monoid_add
-  by default (simp_all add: multiset_eq_iff)
-
 
 subsubsection {* Difference *}