--- a/src/HOL/Library/DAList_Multiset.thy Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/DAList_Multiset.thy Thu Nov 05 10:39:49 2015 +0100
@@ -206,8 +206,8 @@
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)