src/HOL/Transcendental.thy
changeset 57180 74c81a5b5a34
parent 57129 7edb7550663e
child 57275 0ddb5b755cdc
     1.1 --- a/src/HOL/Transcendental.thy	Thu Jun 05 14:37:44 2014 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Fri Jun 06 12:36:06 2014 +0200
     1.3 @@ -1951,6 +1951,9 @@
     1.4  lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
     1.5    unfolding real_of_nat_numeral [symmetric] by (rule powr_realpow)
     1.6  
     1.7 +lemma powr2_sqrt[simp]: "0 < x \<Longrightarrow> sqrt x powr 2 = x"
     1.8 +by(simp add: powr_realpow_numeral)
     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)