diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -15,22 +15,23 @@
 types hypreal = "real star"
 
 abbreviation
-  hypreal_of_real :: "real => real star"
+  hypreal_of_real :: "real => real star" where
   "hypreal_of_real == star_of"
 
 definition
-  omega   :: hypreal   -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
+  omega :: hypreal where   -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
   "omega = star_n (%n. real (Suc n))"
 
-  epsilon :: hypreal   -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
+definition
+  epsilon :: hypreal where   -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
   "epsilon = star_n (%n. inverse (real (Suc n)))"
 
 notation (xsymbols)
-  omega  ("\<omega>")
+  omega  ("\<omega>") and
   epsilon  ("\<epsilon>")
 
 notation (HTML output)
-  omega  ("\<omega>")
+  omega  ("\<omega>") and
   epsilon  ("\<epsilon>")