diff -r e21426f244aa -r 40fe6b80b481 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Fri May 24 23:57:24 2013 +0200
+++ b/src/HOL/Transcendental.thy	Sat May 25 13:59:08 2013 +0200
@@ -1819,6 +1819,9 @@
   apply (subst powr_add, simp, simp)
 done
 
+lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x^(numeral n)"
+  unfolding real_of_nat_numeral[symmetric] by (rule powr_realpow)
+
 lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))"
   apply (case_tac "x = 0", simp, simp)
   apply (rule powr_realpow [THEN sym], simp)