src/HOL/Hyperreal/HyperNat.thy

--- a/src/HOL/Hyperreal/HyperNat.thy	Thu Aug 08 23:51:24 2002 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Thu Aug 08 23:52:55 2002 +0200
@@ -12,13 +12,13 @@
     "hypnatrel == {p. EX X Y. p = ((X::nat=>nat),Y) & 
                        {n::nat. X(n) = Y(n)} : FreeUltrafilterNat}"
 
-typedef hypnat = "UNIV//hypnatrel"              (Equiv.quotient_def)
+typedef hypnat = "UNIV//hypnatrel"              (quotient_def)
 
 instance
    hypnat  :: {ord, zero, one, plus, times, minus}
 
 consts
-  "whn"       :: hypnat               ("whn")  
+  whn       :: hypnat
 
 constdefs