diff -r deb8cac87063 -r 883d559b0b8c src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Mon Oct 08 15:23:20 2001 +0200
@@ -15,10 +15,9 @@
 typedef hypnat = "UNIV//hypnatrel"              (Equiv.quotient_def)
 
 instance
-   hypnat  :: {ord,zero,plus,times,minus}
+   hypnat  :: {ord, zero, one, plus, times, minus}
 
 consts
-  "1hn"       :: hypnat               ("1hn")  
   "whn"       :: hypnat               ("whn")  
 
 constdefs
@@ -54,7 +53,7 @@
   (** hypernatural arithmetic **)
   
   hypnat_zero_def      "0 == Abs_hypnat(hypnatrel``{%n::nat. 0})"
-  hypnat_one_def       "1hn == Abs_hypnat(hypnatrel``{%n::nat. 1})"
+  hypnat_one_def       "1 == Abs_hypnat(hypnatrel``{%n::nat. 1})"
 
   (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
   hypnat_omega_def     "whn == Abs_hypnat(hypnatrel``{%n::nat. n})"