changeset 20730 | da903f59e9ba |
parent 20695 | 1cc6fefbff1a |
child 20740 | 5a103b43da5a |
--- a/src/HOL/Hyperreal/HyperNat.thy Wed Sep 27 05:58:42 2006 +0200 +++ b/src/HOL/Hyperreal/HyperNat.thy Wed Sep 27 07:09:19 2006 +0200 @@ -334,9 +334,6 @@ declare hypreal_of_hypnat_def [transfer_unfold] -lemma HNat_hypreal_of_nat [simp]: "hypreal_of_nat N \<in> Nats" -by (simp add: hypreal_of_nat_def) - lemma hypreal_of_hypnat: "hypreal_of_hypnat (star_n X) = star_n (%n. real (X n))" by (simp add: hypreal_of_hypnat_def starfun)