src/HOL/Hyperreal/HyperDef.thy

--- a/src/HOL/Hyperreal/HyperDef.thy	Thu Aug 08 23:51:24 2002 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Thu Aug 08 23:52:55 2002 +0200
@@ -3,12 +3,12 @@
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : Construction of hyperreals using ultrafilters
-*) 
+*)
 
 HyperDef = Filter + Real +
 
-consts 
- 
+consts
+
     FreeUltrafilterNat   :: nat set set    ("\\<U>")
 
 defs
@@ -19,10 +19,10 @@
 
 constdefs
     hyprel :: "((nat=>real)*(nat=>real)) set"
-    "hyprel == {p. ? X Y. p = ((X::nat=>real),Y) & 
+    "hyprel == {p. ? X Y. p = ((X::nat=>real),Y) &
                    {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}"
 
-typedef hypreal = "UNIV//hyprel"   (Equiv.quotient_def)
+typedef hypreal = "UNIV//hyprel"   (quotient_def)
 
 instance
    hypreal  :: {ord, zero, one, plus, times, minus, inverse}
@@ -38,24 +38,24 @@
   hypreal_minus_def
   "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel``{%n::nat. - (X n)})"
 
-  hypreal_diff_def 
+  hypreal_diff_def
   "x - y == x + -(y::hypreal)"
 
   hypreal_inverse_def
-  "inverse P == Abs_hypreal(UN X: Rep_hypreal(P). 
+  "inverse P == Abs_hypreal(UN X: Rep_hypreal(P).
                     hyprel``{%n. if X n = 0 then 0 else inverse (X n)})"
 
   hypreal_divide_def
   "P / Q::hypreal == P * inverse Q"
-  
+
 constdefs
 
-  hypreal_of_real  :: real => hypreal                 
+  hypreal_of_real  :: real => hypreal
   "hypreal_of_real r         == Abs_hypreal(hyprel``{%n::nat. r})"
 
   omega   :: hypreal   (*an infinite number = [<1,2,3,...>] *)
   "omega == Abs_hypreal(hyprel``{%n::nat. real (Suc n)})"
-    
+
   epsilon :: hypreal   (*an infinitesimal number = [<1,1/2,1/3,...>] *)
   "epsilon == Abs_hypreal(hyprel``{%n::nat. inverse (real (Suc n))})"
 
@@ -63,24 +63,22 @@
   omega   :: hypreal   ("\\<omega>")
   epsilon :: hypreal   ("\\<epsilon>")
 
-  
-defs 
 
-  hypreal_add_def  
+defs
+
+  hypreal_add_def
   "P + Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
                 hyprel``{%n::nat. X n + Y n})"
 
-  hypreal_mult_def  
+  hypreal_mult_def
   "P * Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
                 hyprel``{%n::nat. X n * Y n})"
 
   hypreal_less_def
-  "P < (Q::hypreal) == EX X Y. X: Rep_hypreal(P) & 
-                               Y: Rep_hypreal(Q) & 
+  "P < (Q::hypreal) == EX X Y. X: Rep_hypreal(P) &
+                               Y: Rep_hypreal(Q) &
                                {n::nat. X n < Y n} : FreeUltrafilterNat"
   hypreal_le_def
-  "P <= (Q::hypreal) == ~(Q < P)" 
+  "P <= (Q::hypreal) == ~(Q < P)"
 
 end
- 
-