--- a/src/HOL/Hyperreal/HyperDef.thy Wed Sep 27 05:39:29 2006 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy Wed Sep 27 05:58:42 2006 +0200
@@ -84,6 +84,16 @@
lemma star_of_of_real [simp]: "star_of (of_real r) = of_real r"
by transfer (rule refl)
+lemma of_real_eq_star_of [simp]: "of_real = star_of"
+proof
+ fix r :: real
+ show "of_real r = star_of r"
+ by transfer simp
+qed
+
+lemma Reals_eq_Standard: "(Reals :: hypreal set) = Standard"
+by (simp add: Reals_def Standard_def of_real_eq_star_of)
+
subsection{*Existence of Free Ultrafilter over the Naturals*}
--- a/src/HOL/Hyperreal/NSA.thy Wed Sep 27 05:39:29 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Wed Sep 27 05:58:42 2006 +0200
@@ -46,17 +46,8 @@
const_syntax (HTML output)
approx (infixl "\<approx>" 50)
-
-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)
-
+by (simp add: Reals_def image_def)
subsection {* Nonstandard Extension of the Norm Function *}