--- a/src/HOL/RealDef.thy Sun Mar 07 08:40:38 2010 -0800
+++ b/src/HOL/RealDef.thy Sun Mar 07 09:21:16 2010 -0800
@@ -701,6 +701,9 @@
lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x"
by (insert real_of_int_div2 [of n x], simp)
+lemma Ints_real_of_int [simp]: "real (x::int) \<in> Ints"
+unfolding real_of_int_def by (rule Ints_of_int)
+
subsection{*Embedding the Naturals into the Reals*}
@@ -852,6 +855,12 @@
apply (simp only: real_of_int_real_of_nat)
done
+lemma Nats_real_of_nat [simp]: "real (n::nat) \<in> Nats"
+unfolding real_of_nat_def by (rule of_nat_in_Nats)
+
+lemma Ints_real_of_nat [simp]: "real (n::nat) \<in> Ints"
+unfolding real_of_nat_def by (rule Ints_of_nat)
+
subsection{* Rationals *}