add realpow_pos_nth2 back in

--- 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: