src/HOL/NthRoot.thy

--- a/src/HOL/NthRoot.thy	Wed Jun 18 15:23:40 2014 +0200
+++ b/src/HOL/NthRoot.thy	Wed Jun 18 07:31:12 2014 +0200
@@ -538,6 +538,10 @@
   shows "4 * x\<^sup>2 = (2 * x)\<^sup>2"
 by (simp add: power2_eq_square)
 
+lemma sqrt_at_top: "LIM x at_top. sqrt x :: real :> at_top"
+  by (rule filterlim_at_top_at_top[where Q="\<lambda>x. True" and P="\<lambda>x. 0 < x" and g="power2"])
+     (auto intro: eventually_gt_at_top)
+
 subsection {* Square Root of Sum of Squares *}
 
 lemma sum_squares_bound: