Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix proof of hypreal_sqrt_sum_squares_ge1
authorhuffman
Tue, 08 May 2007 05:06:04 +0200
changeset 22859 c03c076d9dca
parent 22858 5ca5d1cce388
child 22860 107b54207dae
fix proof of hypreal_sqrt_sum_squares_ge1
src/HOL/Hyperreal/HTranscendental.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle