--- 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*}