src/HOL/Hyperreal/HyperDef.thy
changeset 19380 b808efaa5828
parent 17429 e8d6ed3aacfe
child 19765 dfe940911617
     1.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Sun Apr 09 18:51:11 2006 +0200
     1.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Sun Apr 09 18:51:13 2006 +0200
     1.3 @@ -14,8 +14,9 @@
     1.4  
     1.5  types hypreal = "real star"
     1.6  
     1.7 -syntax hypreal_of_real :: "real => real star"
     1.8 -translations "hypreal_of_real" => "star_of :: real => real star"
     1.9 +abbreviation
    1.10 +  hypreal_of_real :: "real => real star"
    1.11 +  "hypreal_of_real == star_of"
    1.12  
    1.13  constdefs
    1.14