# HG changeset patch
# User huffman
# Date 1179645664 -7200
# Node ID 17f7d831efe2204ddfc1828623de658eb8e3458c
# Parent  12f35ece221f77d30e94ff4f0e8613e92a39b9fc
add realpow_pos_nth2 back in

diff -r 12f35ece221f -r 17f7d831efe2 src/HOL/Hyperreal/NthRoot.thy
--- a/src/HOL/Hyperreal/NthRoot.thy	Sun May 20 09:05:44 2007 +0200
+++ b/src/HOL/Hyperreal/NthRoot.thy	Sun May 20 09:21:04 2007 +0200
@@ -37,6 +37,10 @@
   thus ?thesis ..
 qed
 
+(* Used by Integration/RealRandVar.thy in AFP *)
+lemma realpow_pos_nth2: "(0::real) < a \<Longrightarrow> \<exists>r>0. r ^ Suc n = a"
+by (blast intro: realpow_pos_nth)
+
 text {* Uniqueness of nth positive root *}
 
 lemma realpow_pos_nth_unique: