src/HOL/Hyperreal/HTranscendental.thy

--- a/src/HOL/Hyperreal/HTranscendental.thy	Tue May 08 04:56:28 2007 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Tue May 08 05:06:04 2007 +0200
@@ -131,7 +131,7 @@
 done
 
 lemma hypreal_sqrt_sum_squares_ge1 [simp]: "!!x y. x \<le> ( *f* sqrt)(x ^ 2 + y ^ 2)"
-by (transfer, simp)
+by transfer (rule real_sqrt_sum_squares_ge1)
 
 lemma HFinite_hypreal_sqrt:
      "[| 0 \<le> x; x \<in> HFinite |] ==> ( *f* sqrt) x \<in> HFinite"