--- a/src/HOL/Hyperreal/NSA.thy Sat Sep 16 18:04:14 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Sat Sep 16 19:12:03 2006 +0200
@@ -47,10 +47,15 @@
approx (infixl "\<approx>" 50)
-defs (overloaded)
- SReal_def: "Reals == {x. \<exists>r. x = hypreal_of_real r}"
- --{*the standard real numbers as a subset of the hyperreals*}
+lemma hypreal_of_real_of_real_eq: "hypreal_of_real r = of_real r"
+proof -
+ have "hypreal_of_real r = hypreal_of_real (of_real r)" by simp
+ also have "\<dots> = of_real r" by (rule star_of_of_real)
+ finally show ?thesis .
+qed
+lemma SReal_def: "Reals == {x. \<exists>r. x = hypreal_of_real r}"
+by (simp add: Reals_def image_def hypreal_of_real_of_real_eq)
subsection{*Nonstandard extension of the norm function*}