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]