src/HOL/Nonstandard_Analysis/HyperNat.thy

 
 lemma Nats_diff [simp]: "a \<in> Nats \<Longrightarrow> b \<in> Nats \<Longrightarrow> a - b \<in> Nats" for a b :: hypnat
   by (simp add: Nats_eq_Standard)
 
 
-subsection \<open>Infinite Hypernatural Numbers -- @{term HNatInfinite}\<close>
+subsection \<open>Infinite Hypernatural Numbers -- \<^term>\<open>HNatInfinite\<close>\<close>
 
 text \<open>The set of infinite hypernatural numbers.\<close>
 definition HNatInfinite :: "hypnat set"
   where "HNatInfinite = {n. n \<notin> Nats}"
 

   by (simp add: Nats_less_whn)
 
 
 subsubsection \<open>Alternative characterization of the set of infinite hypernaturals\<close>
 
-text \<open>@{term "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"}\<close>
+text \<open>\<^term>\<open>HNatInfinite = {N. \<forall>n \<in> Nats. n < N}\<close>\<close>
 
 (*??delete? similar reasoning in hypnat_omega_gt_SHNat above*)
 lemma HNatInfinite_FreeUltrafilterNat_lemma:
   assumes "\<forall>N::nat. eventually (\<lambda>n. f n \<noteq> N) \<U>"
   shows "eventually (\<lambda>n. N < f n) \<U>"

   apply (safe intro!: Nats_less_HNatInfinite)
   apply (auto simp add: HNatInfinite_def)
   done
 
 
-subsubsection \<open>Alternative Characterization of @{term HNatInfinite} using Free Ultrafilter\<close>
+subsubsection \<open>Alternative Characterization of \<^term>\<open>HNatInfinite\<close> using Free Ultrafilter\<close>
 
 lemma HNatInfinite_FreeUltrafilterNat:
   "star_n X \<in> HNatInfinite \<Longrightarrow> \<forall>u. eventually (\<lambda>n. u < X n) \<U>"
   apply (auto simp add: HNatInfinite_iff SHNat_eq)
   apply (drule_tac x="star_of u" in spec, simp)