| changeset 19380 | b808efaa5828 |
| parent 17433 | 4cf2e7980529 |
| child 19765 | dfe940911617 |
--- a/src/HOL/Hyperreal/HyperNat.thy Sun Apr 09 18:51:11 2006 +0200 +++ b/src/HOL/Hyperreal/HyperNat.thy Sun Apr 09 18:51:13 2006 +0200 @@ -13,8 +13,9 @@ types hypnat = "nat star" -syntax hypnat_of_nat :: "nat => nat star" -translations "hypnat_of_nat" => "star_of :: nat => nat star" +abbreviation + hypnat_of_nat :: "nat => nat star" + "hypnat_of_nat == star_of" subsection{*Properties Transferred from Naturals*}