src/HOL/Library/DAList_Multiset.thy

 
 
 lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<le># m2 \<and> m2 \<le># m1"
   by (metis equal_multiset_def subset_mset.eq_iff)
 
-text \<open>By default the code for @{text "<"} is @{prop"xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> xs = ys"}.
-With equality implemented by @{text"\<le>"}, this leads to three calls of  @{text"\<le>"}.
+text \<open>By default the code for \<open><\<close> is @{prop"xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> xs = ys"}.
+With equality implemented by \<open>\<le>\<close>, this leads to three calls of  \<open>\<le>\<close>.
 Here is a more efficient version:\<close>
 lemma mset_less[code]: "xs <# (ys :: 'a multiset) \<longleftrightarrow> xs \<le># ys \<and> \<not> ys \<le># xs"
   by (rule subset_mset.less_le_not_le)
 
 lemma mset_less_eq_Bag0: