diff -r dbaa38bd223a -r 4a4c14b24800 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Fri Jan 12 14:43:06 2018 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Fri Jan 12 15:27:46 2018 +0100
@@ -188,7 +188,7 @@
 lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
   by (simp add: cofinite_eq_sequentially)
 
-(* legacy names *)
+\<comment> \<open>legacy names\<close>
 lemma Inf_many_def: "Inf_many P \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
 lemma Alm_all_def: "Alm_all P \<longleftrightarrow> \<not> (INFM x. \<not> P x)" by simp
 lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)