--- a/src/HOL/RealDef.thy Tue Feb 23 07:45:54 2010 -0800
+++ b/src/HOL/RealDef.thy Tue Feb 23 10:37:25 2010 -0800
@@ -584,6 +584,11 @@
lemma real_of_int_mult [simp]: "real(x * y) = real (x::int) * real y"
by (simp add: real_of_int_def)
+lemma real_of_int_power [simp]: "real (x ^ n) = real (x::int) ^ n"
+by (simp add: real_of_int_def of_int_power)
+
+lemmas power_real_of_int = real_of_int_power [symmetric]
+
lemma real_of_int_setsum [simp]: "real ((SUM x:A. f x)::int) = (SUM x:A. real(f x))"
apply (subst real_eq_of_int)+
apply (rule of_int_setsum)
@@ -731,6 +736,11 @@
lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n"
by (simp add: real_of_nat_def of_nat_mult)
+lemma real_of_nat_power [simp]: "real (m ^ n) = real (m::nat) ^ n"
+by (simp add: real_of_nat_def of_nat_power)
+
+lemmas power_real_of_nat = real_of_nat_power [symmetric]
+
lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) =
(SUM x:A. real(f x))"
apply (subst real_eq_of_nat)+