src/HOL/Hyperreal/HyperNat.thy
 changeset 21404 eb85850d3eb7 parent 20740 5a103b43da5a child 21787 9edd495b6330
```     1.1 --- a/src/HOL/Hyperreal/HyperNat.thy	Fri Nov 17 02:19:55 2006 +0100
1.2 +++ b/src/HOL/Hyperreal/HyperNat.thy	Fri Nov 17 02:20:03 2006 +0100
1.3 @@ -14,7 +14,7 @@
1.4  types hypnat = "nat star"
1.5
1.6  abbreviation
1.7 -  hypnat_of_nat :: "nat => nat star"
1.8 +  hypnat_of_nat :: "nat => nat star" where
1.9    "hypnat_of_nat == star_of"
1.10
1.11  subsection{*Properties Transferred from Naturals*}
1.12 @@ -161,7 +161,7 @@
1.13
1.14  definition
1.15    (* the set of infinite hypernatural numbers *)
1.16 -  HNatInfinite :: "hypnat set"
1.17 +  HNatInfinite :: "hypnat set" where
1.18    "HNatInfinite = {n. n \<notin> Nats}"
1.19
1.20  lemma Nats_not_HNatInfinite_iff: "(x \<in> Nats) = (x \<notin> HNatInfinite)"
1.21 @@ -254,7 +254,7 @@
1.22
1.23  definition
1.24    (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
1.25 -  whn :: hypnat
1.26 +  whn :: hypnat where
1.27    hypnat_omega_def: "whn = star_n (%n::nat. n)"
1.28
1.29  lemma hypnat_of_nat_neq_whn: "hypnat_of_nat n \<noteq> whn"
1.30 @@ -362,7 +362,7 @@
1.31  text{*Obtained using the nonstandard extension of the naturals*}
1.32
1.33  definition
1.34 -  hypreal_of_hypnat :: "hypnat => hypreal"
1.35 +  hypreal_of_hypnat :: "hypnat => hypreal" where
1.36    "hypreal_of_hypnat = *f* real"
1.37
1.38  declare hypreal_of_hypnat_def [transfer_unfold]
```