src/HOL/Hyperreal/HyperDef.thy
changeset 10919 144ede948e58
parent 10834 a7897aebbffc
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Tue Jan 16 00:40:57 2001 +0100
     1.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Tue Jan 16 12:20:52 2001 +0100
     1.3 @@ -29,9 +29,7 @@
     1.4  
     1.5  consts 
     1.6  
     1.7 -  "1hr"       :: hypreal               ("1hr")  
     1.8 -  "whr"       :: hypreal               ("whr")  
     1.9 -  "ehr"       :: hypreal               ("ehr")  
    1.10 +  "1hr"          :: hypreal               ("1hr")  
    1.11  
    1.12  
    1.13  defs
    1.14 @@ -42,14 +40,6 @@
    1.15    hypreal_one_def
    1.16    "1hr == Abs_hypreal(hyprel``{%n::nat. (#1::real)})"
    1.17  
    1.18 -  (* an infinite number = [<1,2,3,...>] *)
    1.19 -  omega_def
    1.20 -  "whr == Abs_hypreal(hyprel``{%n::nat. real_of_nat (Suc n)})"
    1.21 -    
    1.22 -  (* an infinitesimal number = [<1,1/2,1/3,...>] *)
    1.23 -  epsilon_def
    1.24 -  "ehr == Abs_hypreal(hyprel``{%n::nat. inverse (real_of_nat (Suc n))})"
    1.25 -
    1.26    hypreal_minus_def
    1.27    "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel``{%n::nat. - (X n)})"
    1.28  
    1.29 @@ -68,6 +58,17 @@
    1.30    hypreal_of_real  :: real => hypreal                 
    1.31    "hypreal_of_real r         == Abs_hypreal(hyprel``{%n::nat. r})"
    1.32  
    1.33 +  omega   :: hypreal   (*an infinite number = [<1,2,3,...>] *)
    1.34 +  "omega == Abs_hypreal(hyprel``{%n::nat. real (Suc n)})"
    1.35 +    
    1.36 +  epsilon :: hypreal   (*an infinitesimal number = [<1,1/2,1/3,...>] *)
    1.37 +  "epsilon == Abs_hypreal(hyprel``{%n::nat. inverse (real (Suc n))})"
    1.38 +
    1.39 +syntax (xsymbols)
    1.40 +  omega   :: hypreal   ("\\<omega>")
    1.41 +  epsilon :: hypreal   ("\\<epsilon>")
    1.42 +
    1.43 +  
    1.44  defs 
    1.45  
    1.46    hypreal_add_def