| changeset 21404 | eb85850d3eb7 |
| parent 20730 | da903f59e9ba |
| child 21810 | b2d23672b003 |
--- a/src/HOL/Hyperreal/HyperArith.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOL/Hyperreal/HyperArith.thy Fri Nov 17 02:20:03 2006 +0100 @@ -34,7 +34,7 @@ subsection{*Embedding the Naturals into the Hyperreals*} abbreviation - hypreal_of_nat :: "nat => hypreal" + hypreal_of_nat :: "nat => hypreal" where "hypreal_of_nat == of_nat" lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}"