src/HOL/Transcendental.thy
changeset 52139 40fe6b80b481
parent 51641 cd05e9fcc63d
child 53015 a1119cf551e8
     1.1 --- a/src/HOL/Transcendental.thy	Fri May 24 23:57:24 2013 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Sat May 25 13:59:08 2013 +0200
     1.3 @@ -1819,6 +1819,9 @@
     1.4    apply (subst powr_add, simp, simp)
     1.5  done
     1.6  
     1.7 +lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x^(numeral n)"
     1.8 +  unfolding real_of_nat_numeral[symmetric] by (rule powr_realpow)
     1.9 +
    1.10  lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))"
    1.11    apply (case_tac "x = 0", simp, simp)
    1.12    apply (rule powr_realpow [THEN sym], simp)