diff -r 523124691b3a -r e0b46cd72414 src/HOL/RealPow.thy
--- a/src/HOL/RealPow.thy	Tue Feb 23 07:45:54 2010 -0800
+++ b/src/HOL/RealPow.thy	Tue Feb 23 10:37:25 2010 -0800
@@ -49,11 +49,6 @@
 apply auto
 done
 
-lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)"
-apply (induct "n")
-apply (auto simp add: real_of_nat_one real_of_nat_mult)
-done
-
 lemma realpow_real_of_nat_two_pos [simp] : "0 < real (Suc (Suc 0) ^ n)"
 apply (induct "n")
 apply (auto simp add: zero_less_mult_iff)
@@ -65,21 +60,6 @@
   by (rule power_le_imp_le_base)
 
 
-subsection{*Literal Arithmetic Involving Powers, Type @{typ real}*}
-
-lemma real_of_int_power: "real (x::int) ^ n = real (x ^ n)"
-apply (induct "n")
-apply (simp_all add: nat_mult_distrib)
-done
-declare real_of_int_power [symmetric, simp]
-
-lemma power_real_number_of:
-     "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)"
-by (simp only: real_number_of [symmetric] real_of_int_power)
-
-declare power_real_number_of [of _ "number_of w", standard, simp]
-
-
 subsection{* Squares of Reals *}
 
 lemma real_two_squares_add_zero_iff [simp]: