--- a/src/HOL/Library/Multiset.thy Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Library/Multiset.thy Fri Dec 07 15:07:59 2007 +0100
@@ -49,11 +49,24 @@
set_of :: "'a multiset => 'a set" where
"set_of M = {x. x :# M}"
-instance multiset :: (type) "{plus, minus, zero, size}"
+instantiation multiset :: (type) "{plus, minus, zero, size}"
+begin
+
+definition
union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
+
+definition
diff_def: "M - N == Abs_multiset (\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
+
+definition
Zero_multiset_def [simp]: "0 == {#}"
- size_def: "size M == setsum (count M) (set_of M)" ..
+
+definition
+ size_def: "size M == setsum (count M) (set_of M)"
+
+instance ..
+
+end
definition
multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where