src/HOL/Hyperreal/HyperDef.thy
changeset 11713 883d559b0b8c
parent 11701 3d51fbf81c17
child 12018 ec054019c910
     1.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Mon Oct 08 14:30:28 2001 +0200
     1.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Mon Oct 08 15:23:20 2001 +0200
     1.3 @@ -25,12 +25,7 @@
     1.4  typedef hypreal = "UNIV//hyprel"   (Equiv.quotient_def)
     1.5  
     1.6  instance
     1.7 -   hypreal  :: {ord, zero, plus, times, minus, inverse}
     1.8 -
     1.9 -consts 
    1.10 -
    1.11 -  "1hr"          :: hypreal               ("1hr")  
    1.12 -
    1.13 +   hypreal  :: {ord, zero, one, plus, times, minus, inverse}
    1.14  
    1.15  defs
    1.16  
    1.17 @@ -38,7 +33,7 @@
    1.18    "0 == Abs_hypreal(hyprel``{%n::nat. (Numeral0::real)})"
    1.19  
    1.20    hypreal_one_def
    1.21 -  "1hr == Abs_hypreal(hyprel``{%n::nat. (Numeral1::real)})"
    1.22 +  "1 == Abs_hypreal(hyprel``{%n::nat. (Numeral1::real)})"
    1.23  
    1.24    hypreal_minus_def
    1.25    "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel``{%n::nat. - (X n)})"