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