src/HOL/Library/Multiset.thy
changeset 14691 e1eedc8cad37
parent 14445 4392cb82018b
child 14706 71590b7733b7
     1.1 --- a/src/HOL/Library/Multiset.thy	Sat May 01 21:59:12 2004 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Sat May 01 22:01:57 2004 +0200
     1.3 @@ -46,9 +46,7 @@
     1.4    set_of :: "'a multiset => 'a set"
     1.5    "set_of M == {x. x :# M}"
     1.6  
     1.7 -instance multiset :: (type) plus ..
     1.8 -instance multiset :: (type) minus ..
     1.9 -instance multiset :: (type) zero ..
    1.10 +instance multiset :: (type) "{plus, minus, zero}" ..
    1.11  
    1.12  defs (overloaded)
    1.13    union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"