diff -r 30d0b2f1df76 -r a79c1080f1e9 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Mar 02 21:16:02 2017 +0100
+++ b/src/HOL/Transcendental.thy	Sun Mar 05 10:57:51 2017 +0100
@@ -2694,6 +2694,10 @@
 lemma powr_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
   by (metis of_nat_numeral powr_realpow)
 
+lemma numeral_powr_numeral[simp]:
+  "(numeral m :: real) powr (numeral n :: real) = numeral m ^ (numeral n)"
+by(simp add: powr_numeral)
+
 lemma powr_real_of_int:
   "x > 0 \<Longrightarrow> x powr real_of_int n = (if n \<ge> 0 then x ^ nat n else inverse (x ^ nat (- n)))"
   using powr_realpow[of x "nat n"] powr_realpow[of x "nat (-n)"]
@@ -2755,7 +2759,7 @@
   by (simp add: root_powr_inverse ln_powr)
 
 lemma ln_sqrt: "0 < x \<Longrightarrow> ln (sqrt x) = ln x / 2"
-  by (simp add: ln_powr powr_numeral ln_powr[symmetric] mult.commute)
+  by (simp add: ln_powr ln_powr[symmetric] mult.commute)
 
 lemma log_root: "n > 0 \<Longrightarrow> a > 0 \<Longrightarrow> log b (root n a) =  log b a / n"
   by (simp add: log_def ln_root)