src/HOL/Hyperreal/HyperDef.thy
changeset 12018 ec054019c910
parent 11713 883d559b0b8c
child 13487 1291c6375c29
     1.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Thu Nov 01 21:12:13 2001 +0100
     1.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Fri Nov 02 17:55:24 2001 +0100
     1.3 @@ -30,10 +30,10 @@
     1.4  defs
     1.5  
     1.6    hypreal_zero_def
     1.7 -  "0 == Abs_hypreal(hyprel``{%n::nat. (Numeral0::real)})"
     1.8 +  "0 == Abs_hypreal(hyprel``{%n::nat. (0::real)})"
     1.9  
    1.10    hypreal_one_def
    1.11 -  "1 == Abs_hypreal(hyprel``{%n::nat. (Numeral1::real)})"
    1.12 +  "1 == Abs_hypreal(hyprel``{%n::nat. (1::real)})"
    1.13  
    1.14    hypreal_minus_def
    1.15    "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel``{%n::nat. - (X n)})"
    1.16 @@ -43,7 +43,7 @@
    1.17  
    1.18    hypreal_inverse_def
    1.19    "inverse P == Abs_hypreal(UN X: Rep_hypreal(P). 
    1.20 -                    hyprel``{%n. if X n = Numeral0 then Numeral0 else inverse (X n)})"
    1.21 +                    hyprel``{%n. if X n = 0 then 0 else inverse (X n)})"
    1.22  
    1.23    hypreal_divide_def
    1.24    "P / Q::hypreal == P * inverse Q"