src/HOL/Hyperreal/HyperNat.thy

 begin
 
 types hypnat = "nat star"
 
 abbreviation
-  hypnat_of_nat :: "nat => nat star"
+  hypnat_of_nat :: "nat => nat star" where
   "hypnat_of_nat == star_of"
 
 subsection{*Properties Transferred from Naturals*}
 
 lemma hypnat_minus_zero [simp]: "!!z. z - z = (0::hypnat)"

 
 subsection{*Infinite Hypernatural Numbers -- @{term HNatInfinite}*}
 
 definition
   (* the set of infinite hypernatural numbers *)
-  HNatInfinite :: "hypnat set"
+  HNatInfinite :: "hypnat set" where
   "HNatInfinite = {n. n \<notin> Nats}"
 
 lemma Nats_not_HNatInfinite_iff: "(x \<in> Nats) = (x \<notin> HNatInfinite)"
 by (simp add: HNatInfinite_def)
 

 
 subsection{*Existence of an infinite hypernatural number*}
 
 definition
   (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
-  whn :: hypnat
+  whn :: hypnat where
   hypnat_omega_def: "whn = star_n (%n::nat. n)"
 
 lemma hypnat_of_nat_neq_whn: "hypnat_of_nat n \<noteq> whn"
 by (simp add: hypnat_omega_def star_of_def star_n_eq_iff FUFNat.finite)
 

 
 subsection{*Embedding of the Hypernaturals into the Hyperreals*}
 text{*Obtained using the nonstandard extension of the naturals*}
 
 definition
-  hypreal_of_hypnat :: "hypnat => hypreal"
+  hypreal_of_hypnat :: "hypnat => hypreal" where
   "hypreal_of_hypnat = *f* real"
 
 declare hypreal_of_hypnat_def [transfer_unfold]
 
 lemma hypreal_of_hypnat: