src/HOL/Library/Multiset.thy

 
 interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op \<subseteq>#" "op \<subset>#"
   by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
     \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
 
-interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "op +" 0 "op -" "op \<le>#" "op <#"
+interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "op +" 0 "op -" "op \<subseteq>#" "op \<subset>#"
   by standard
     \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
 
 lemma mset_subset_eqI:
   "(\<And>a. count A a \<le> count B a) \<Longrightarrow> A \<subseteq># B"

   apply (rule iffI)
    apply (rule exI [where x = "B - A"])
    apply (auto intro: multiset_eq_iff [THEN iffD2])
   done
 
-interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" 0 "op \<le>#" "op <#" "op -"
+interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" 0 "op \<subseteq>#" "op \<subset>#" "op -"
   by standard (simp, fact mset_subset_eq_exists_conv)
     \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
 
 declare subset_mset.add_diff_assoc[simp] subset_mset.add_diff_assoc2[simp]
 

   by (rule mset_subset_eq_insertD) simp
 
 lemma mset_subset_of_empty[simp]: "A \<subset># {#} \<longleftrightarrow> False"
   by (simp only: subset_mset.not_less_zero)
 
-lemma empty_subset_add_mset[simp]: "{#} <# add_mset x M"
-by(auto intro: subset_mset.gr_zeroI)
+lemma empty_subset_add_mset[simp]: "{#} \<subset># add_mset x M"
+  by (auto intro: subset_mset.gr_zeroI)
 
 lemma empty_le: "{#} \<subseteq># A"
   by (fact subset_mset.zero_le)
 
 lemma insert_subset_eq_iff: