src/HOL/Hyperreal/HyperNat.thy

 lemma hypnat_of_nat_minus:
       "hypnat_of_nat ((j::nat) - k) = hypnat_of_nat j - hypnat_of_nat k"
 by (simp add: hypnat_of_nat_def split: nat_diff_split hypnat_diff_split)
 
 
-subsection{*Existence of an Infinite Hypernatural Number*}
+subsection{*Existence of an infinite hypernatural number*}
 
 lemma hypnat_omega: "hypnatrel``{%n::nat. n} \<in> hypnat"
 by auto
 
 lemma Rep_hypnat_omega: "Rep_hypnat(whn) \<in> hypnat"

 text{*Existence of infinite number not corresponding to any natural number
 follows because member @{term FreeUltrafilterNat} is not finite.
 See @{text HyperDef.thy} for similar argument.*}
 
 
-subsection{*Properties of the set @{term Nats} of Embedded Natural Numbers*}
+subsection{*Properties of the set of embedded natural numbers*}
 
 lemma of_nat_eq_add [rule_format]:
      "\<forall>d::hypnat. of_nat m = of_nat n + d --> d \<in> range of_nat"
 apply (induct n) 
 apply (auto simp add: add_assoc) 

 
 lemma HNatInfinite_not_Nats_iff: "(x \<in> HNatInfinite) = (x \<notin> Nats)"
 by (simp add: HNatInfinite_def)
 
 
-subsection{*Alternative Characterization of the Set of Infinite Hypernaturals:
-@{term "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"}*}
+subsection{*Alternative characterization of the set of infinite hypernaturals*}
+
+text{* @{term "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"}*}
 
 (*??delete? similar reasoning in hypnat_omega_gt_SHNat above*)
 lemma HNatInfinite_FreeUltrafilterNat_lemma:
      "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat
       ==> {n. N < f n} \<in> FreeUltrafilterNat"