# HG changeset patch
# User huffman
# Date 1159311179 -7200
# Node ID 4c4869e4ddb76e241b93cf6b0a1e413e23ea5c7e
# Parent  2244b0d719a06e976482a1c7538aea2cbe294f42
add lemmas of_int_in_Reals, of_nat_in_Reals

diff -r 2244b0d719a0 -r 4c4869e4ddb7 src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Tue Sep 26 22:37:51 2006 +0200
+++ b/src/HOL/Real/RealVector.thy	Wed Sep 27 00:52:59 2006 +0200
@@ -251,6 +251,12 @@
 lemma of_real_in_Reals [simp]: "of_real r \<in> Reals"
 by (simp add: Reals_def)
 
+lemma of_int_in_Reals [simp]: "of_int z \<in> Reals"
+by (subst of_real_of_int_eq [symmetric], rule of_real_in_Reals)
+
+lemma of_nat_in_Reals [simp]: "of_nat n \<in> Reals"
+by (subst of_real_of_nat_eq [symmetric], rule of_real_in_Reals)
+
 lemma Reals_0 [simp]: "0 \<in> Reals"
 apply (unfold Reals_def)
 apply (rule range_eqI)