# HG changeset patch
# User paulson
# Date 959098746 -7200
# Node ID 9660ca91828ccc9e5f3eac0060b4d1bf96d9fe44
# Parent  7328d7c8d20181bc54112b2bcaa47eff00d22b82
Multisets have a zero: the empty multiset

diff -r 7328d7c8d201 -r 9660ca91828c src/HOL/Induct/Multiset.thy
--- 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                        ("{#}")