src/HOL/Library/Multiset.thy
changeset 12338 de0f4a63baa5
parent 11868 56db9f3a6b3e
child 12399 2ba27248af7f
     1.1 --- a/src/HOL/Library/Multiset.thy	Sat Dec 01 18:51:46 2001 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Sat Dec 01 18:52:32 2001 +0100
     1.3 @@ -47,9 +47,9 @@
     1.4    set_of :: "'a multiset => 'a set"
     1.5    "set_of M == {x. x :# M}"
     1.6  
     1.7 -instance multiset :: ("term") plus ..
     1.8 -instance multiset :: ("term") minus ..
     1.9 -instance multiset :: ("term") zero ..
    1.10 +instance multiset :: (type) plus ..
    1.11 +instance multiset :: (type) minus ..
    1.12 +instance multiset :: (type) zero ..
    1.13  
    1.14  defs (overloaded)
    1.15    union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
    1.16 @@ -114,7 +114,7 @@
    1.17  
    1.18  theorems union_ac = union_assoc union_commute union_lcomm
    1.19  
    1.20 -instance multiset :: ("term") plus_ac0
    1.21 +instance multiset :: (type) plus_ac0
    1.22    apply intro_classes
    1.23      apply (rule union_commute)
    1.24     apply (rule union_assoc)
    1.25 @@ -660,7 +660,7 @@
    1.26  
    1.27  subsubsection {* Partial-order properties *}
    1.28  
    1.29 -instance multiset :: ("term") ord ..
    1.30 +instance multiset :: (type) ord ..
    1.31  
    1.32  defs (overloaded)
    1.33    less_multiset_def: "M' < M == (M', M) \<in> mult {(x', x). x' < x}"