src/HOL/Hyperreal/NthRoot.thy
changeset 22968 7134874437ac
parent 22961 e499ded5d0fc
child 23009 01c295dd4a36
     1.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Mon May 14 17:45:42 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Mon May 14 18:03:25 2007 +0200
     1.3 @@ -475,7 +475,7 @@
     1.4  subsection {* Square Root of Sum of Squares *}
     1.5  
     1.6  lemma real_sqrt_mult_self_sum_ge_zero [simp]: "0 \<le> sqrt(x*x + y*y)"
     1.7 -by (rule real_sqrt_ge_zero [OF real_mult_self_sum_ge_zero])
     1.8 +by (rule real_sqrt_ge_zero [OF sum_squares_ge_zero])
     1.9  
    1.10  lemma real_sqrt_sum_squares_ge_zero [simp]: "0 \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
    1.11  by simp