# HG changeset patch
# User nipkow
# Date 1402050966 -7200
# Node ID 74c81a5b5a340a21803695815b4c610efb295315
# Parent  011955e7846bf2088eedbafbecba38f729f79cab
added lemma

diff -r 011955e7846b -r 74c81a5b5a34 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Jun 05 14:37:44 2014 +0200
+++ b/src/HOL/Transcendental.thy	Fri Jun 06 12:36:06 2014 +0200
@@ -1951,6 +1951,9 @@
 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 powr2_sqrt[simp]: "0 < x \<Longrightarrow> sqrt x powr 2 = x"
+by(simp add: powr_realpow_numeral)
+
 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)