author nipkow Wed, 21 Jul 2004 08:35:29 +0200 changeset 15070 541d2a35fc30 parent 15069 0a0371b55a0f child 15071 b65fc0787fbe
Fixed latex problem
```--- a/src/HOL/Hyperreal/HyperNat.thy	Tue Jul 20 16:07:45 2004 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Wed Jul 21 08:35:29 2004 +0200
@@ -504,7 +504,7 @@
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
@@ -517,7 +517,7 @@
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*}

"\<forall>d::hypnat. of_nat m = of_nat n + d --> d \<in> range of_nat"
@@ -591,8 +591,9 @@

-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:```