diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Hyperreal/HyperNat.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -14,7 +14,7 @@
 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*}
@@ -161,7 +161,7 @@
 
 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)"
@@ -254,7 +254,7 @@
 
 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"
@@ -362,7 +362,7 @@
 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]