src/HOL/Library/Multiset.thy

 end
 
 text \<open>
   A note on code generation: When defining some function containing a
   subterm @{term "fold_mset F"}, code generation is not automatic. When
-  interpreting locale @{text left_commutative} with @{text F}, the
+  interpreting locale \<open>left_commutative\<close> with \<open>F\<close>, the
   would be code thms for @{const fold_mset} become thms like
-  @{term "fold_mset F z {#} = z"} where @{text F} is not a pattern but
+  @{term "fold_mset F z {#} = z"} where \<open>F\<close> is not a pattern but
   contains defined symbols, i.e.\ is not a code thm. Hence a separate
-  constant with its own code thms needs to be introduced for @{text
-  F}. See the image operator below.
+  constant with its own code thms needs to be introduced for \<open>F\<close>. See the image operator below.
 \<close>
 
 
 subsection \<open>Image\<close>
 

   next
     case True from True \<open>x \<notin> A\<close> show ?thesis by (induct A) auto
   qed
   then show "PROP ?P" "PROP ?Q" "PROP ?R"
   by (auto elim!: Set.set_insert)
-qed -- \<open>TODO: maybe define @{const mset_set} also in terms of @{const Abs_multiset}\<close>
+qed \<comment> \<open>TODO: maybe define @{const mset_set} also in terms of @{const Abs_multiset}\<close>
 
 lemma elem_mset_set[simp, intro]: "finite A \<Longrightarrow> x \<in># mset_set A \<longleftrightarrow> x \<in> A"
   by (induct A rule: finite_induct) simp_all
 
 context linorder

   "mset (sort_key k xs) = mset xs"
   by (induct xs) (simp_all add: ac_simps)
 
 text \<open>
   This lemma shows which properties suffice to show that a function
-  @{text "f"} with @{text "f xs = ys"} behaves like sort.
+  \<open>f\<close> with \<open>f xs = ys\<close> behaves like sort.
 \<close>
 
 lemma properties_for_sort_key:
   assumes "mset ys = mset xs"
     and "\<And>k. k \<in> set ys \<Longrightarrow> filter (\<lambda>x. f k = f x) ys = filter (\<lambda>x. f k = f x) xs"

 
 declare set_mset_mset [code]
 
 declare sorted_list_of_multiset_mset [code]
 
-lemma [code]: -- \<open>not very efficient, but representation-ignorant!\<close>
+lemma [code]: \<comment> \<open>not very efficient, but representation-ignorant!\<close>
   "mset_set A = mset (sorted_list_of_set A)"
   apply (cases "finite A")
   apply simp_all
   apply (induct A rule: finite_induct)
   apply (simp_all add: add.commute)