1.1 --- a/src/HOL/Hyperreal/HyperNat.thy	Tue Jul 20 16:07:45 2004 +0200
     1.2 +++ b/src/HOL/Hyperreal/HyperNat.thy	Wed Jul 21 08:35:29 2004 +0200
     1.3 @@ -504,7 +504,7 @@
     1.4  by (simp add: hypnat_of_nat_def split: nat_diff_split hypnat_diff_split)
     1.5  
     1.6  
     1.7 -subsection{*Existence of an Infinite Hypernatural Number*}
     1.8 +subsection{*Existence of an infinite hypernatural number*}
     1.9  
    1.10  lemma hypnat_omega: "hypnatrel``{%n::nat. n} \<in> hypnat"
    1.11  by auto
    1.12 @@ -517,7 +517,7 @@
    1.13  See @{text HyperDef.thy} for similar argument.*}
    1.14  
    1.15  
    1.16 -subsection{*Properties of the set @{term Nats} of Embedded Natural Numbers*}
    1.17 +subsection{*Properties of the set of embedded natural numbers*}
    1.18  
    1.19  lemma of_nat_eq_add [rule_format]:
    1.20       "\<forall>d::hypnat. of_nat m = of_nat n + d --> d \<in> range of_nat"
    1.21 @@ -591,8 +591,9 @@
    1.22  by (simp add: HNatInfinite_def)
    1.23  
    1.24  
    1.25 -subsection{*Alternative Characterization of the Set of Infinite Hypernaturals:
    1.26 -@{term "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"}*}
    1.27 +subsection{*Alternative characterization of the set of infinite hypernaturals*}
    1.28 +
    1.29 +text{* @{term "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"}*}
    1.30  
    1.31  (*??delete? similar reasoning in hypnat_omega_gt_SHNat above*)
    1.32  lemma HNatInfinite_FreeUltrafilterNat_lemma: