src/HOL/Library/Infinite_Set.thy

 subsection "Infinite Sets"
 
 text \<open>
   Some elementary facts about infinite sets, mostly by Stephan Merz.
   Beware! Because "infinite" merely abbreviates a negation, these
-  lemmas may not work well with @{text "blast"}.
+  lemmas may not work well with \<open>blast\<close>.
 \<close>
 
 abbreviation infinite :: "'a set \<Rightarrow> bool"
   where "infinite S \<equiv> \<not> finite S"
 

 lemma finite_nat_bounded: "finite (S::nat set) \<Longrightarrow> \<exists>k. S \<subseteq> {..<k}"
   by (simp add: finite_nat_iff_bounded)
 
 text \<open>
   For a set of natural numbers to be infinite, it is enough to know
-  that for any number larger than some @{text k}, there is some larger
+  that for any number larger than some \<open>k\<close>, there is some larger
   number that is an element of the set.
 \<close>
 
 lemma unbounded_k_infinite: "\<forall>m>k. \<exists>n>m. n \<in> S \<Longrightarrow> infinite (S::nat set)"
   by (metis (full_types) infinite_nat_iff_unbounded_le le_imp_less_Suc not_less