# HG changeset patch
# User huffman
# Date 1178593564 -7200
# Node ID c03c076d9dca8c3d096f5cc29c4c1844528acb94
# Parent  5ca5d1cce388318f7d7e6fc2e532f04c953a7fb6
fix proof of hypreal_sqrt_sum_squares_ge1

diff -r 5ca5d1cce388 -r c03c076d9dca 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"