src/HOL/Library/Multiset.thy

 
 constdefs
   set_of :: "'a multiset => 'a set"
   "set_of M == {x. x :# M}"
 
-instance multiset :: ("term") plus ..
-instance multiset :: ("term") minus ..
-instance multiset :: ("term") zero ..
+instance multiset :: (type) plus ..
+instance multiset :: (type) minus ..
+instance multiset :: (type) zero ..
 
 defs (overloaded)
   union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
   diff_def: "M - N == Abs_multiset (\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
   Zero_multiset_def [simp]: "0 == {#}"

   apply (rule union_commute [THEN arg_cong])
   done
 
 theorems union_ac = union_assoc union_commute union_lcomm
 
-instance multiset :: ("term") plus_ac0
+instance multiset :: (type) plus_ac0
   apply intro_classes
     apply (rule union_commute)
    apply (rule union_assoc)
   apply simp
   done

   done
 
 
 subsubsection {* Partial-order properties *}
 
-instance multiset :: ("term") ord ..
+instance multiset :: (type) ord ..
 
 defs (overloaded)
   less_multiset_def: "M' < M == (M', M) \<in> mult {(x', x). x' < x}"
   le_multiset_def: "M' <= M == M' = M \<or> M' < (M::'a multiset)"