| changeset 19380 | b808efaa5828 |
| parent 17429 | e8d6ed3aacfe |
| child 19765 | dfe940911617 |
--- a/src/HOL/Hyperreal/HyperDef.thy Sun Apr 09 18:51:11 2006 +0200 +++ b/src/HOL/Hyperreal/HyperDef.thy Sun Apr 09 18:51:13 2006 +0200 @@ -14,8 +14,9 @@ types hypreal = "real star" -syntax hypreal_of_real :: "real => real star" -translations "hypreal_of_real" => "star_of :: real => real star" +abbreviation + hypreal_of_real :: "real => real star" + "hypreal_of_real == star_of" constdefs