src/HOL/Nonstandard_Analysis/HyperNat.thy
changeset 69597 ff784d5a5bfb
parent 67091 1393c2340eec
     1.1 --- a/src/HOL/Nonstandard_Analysis/HyperNat.thy	Sat Jan 05 17:00:43 2019 +0100
     1.2 +++ b/src/HOL/Nonstandard_Analysis/HyperNat.thy	Sat Jan 05 17:24:33 2019 +0100
     1.3 @@ -165,7 +165,7 @@
     1.4    by (simp add: Nats_eq_Standard)
     1.5  
     1.6  
     1.7 -subsection \<open>Infinite Hypernatural Numbers -- @{term HNatInfinite}\<close>
     1.8 +subsection \<open>Infinite Hypernatural Numbers -- \<^term>\<open>HNatInfinite\<close>\<close>
     1.9  
    1.10  text \<open>The set of infinite hypernatural numbers.\<close>
    1.11  definition HNatInfinite :: "hypnat set"
    1.12 @@ -306,7 +306,7 @@
    1.13  
    1.14  subsubsection \<open>Alternative characterization of the set of infinite hypernaturals\<close>
    1.15  
    1.16 -text \<open>@{term "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"}\<close>
    1.17 +text \<open>\<^term>\<open>HNatInfinite = {N. \<forall>n \<in> Nats. n < N}\<close>\<close>
    1.18  
    1.19  (*??delete? similar reasoning in hypnat_omega_gt_SHNat above*)
    1.20  lemma HNatInfinite_FreeUltrafilterNat_lemma:
    1.21 @@ -326,7 +326,7 @@
    1.22    done
    1.23  
    1.24  
    1.25 -subsubsection \<open>Alternative Characterization of @{term HNatInfinite} using Free Ultrafilter\<close>
    1.26 +subsubsection \<open>Alternative Characterization of \<^term>\<open>HNatInfinite\<close> using Free Ultrafilter\<close>
    1.27  
    1.28  lemma HNatInfinite_FreeUltrafilterNat:
    1.29    "star_n X \<in> HNatInfinite \<Longrightarrow> \<forall>u. eventually (\<lambda>n. u < X n) \<U>"