src/HOL/Library/Multiset.thy

--- a/src/HOL/Library/Multiset.thy	Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Library/Multiset.thy	Sat May 01 22:01:57 2004 +0200
@@ -46,9 +46,7 @@
   set_of :: "'a multiset => 'a set"
   "set_of M == {x. x :# M}"
 
-instance multiset :: (type) plus ..
-instance multiset :: (type) minus ..
-instance multiset :: (type) zero ..
+instance multiset :: (type) "{plus, minus, zero}" ..
 
 defs (overloaded)
   union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"