Multisets have a zero: the empty multiset

--- a/src/HOL/Induct/Multiset.thy	Tue May 23 18:14:57 2000 +0200
+++ b/src/HOL/Induct/Multiset.thy	Tue May 23 18:19:06 2000 +0200
@@ -14,7 +14,7 @@
 typedef
   'a multiset = "{f :: 'a => nat . finite{x . 0 < f x}}" (multiset_witness)
 
-instance multiset :: (term){ord,plus,minus}
+instance multiset :: (term){ord,zero,plus,minus}
 
 consts
   "{#}"  :: 'a multiset                        ("{#}")