# HG changeset patch
# User wenzelm
# Date 1085166910 -7200
# Node ID d2b071e65e4cd274917dcf89145f1fe9671cb1e1
# Parent  c0401da7726da5b7e7e1643e006bacdb2d19a440
tuned document;

diff -r c0401da7726d -r d2b071e65e4c src/HOL/Hyperreal/NthRoot.thy
--- a/src/HOL/Hyperreal/NthRoot.thy	Fri May 21 21:14:52 2004 +0200
+++ b/src/HOL/Hyperreal/NthRoot.thy	Fri May 21 21:15:10 2004 +0200
@@ -8,10 +8,13 @@
 
 theory NthRoot = SEQ + HSeries:
 
-text{*Various lemmas needed for this result. We follow the proof
-   given by John Lindsay Orr (jorr@math.unl.edu) in his Analysis
-   Webnotes available on the www at http://www.math.unl.edu/~webnotes
-   Lemmas about sequences of reals are used to reach the result.*}
+text {*
+  Various lemmas needed for this result. We follow the proof given by
+  John Lindsay Orr (\texttt{jorr@math.unl.edu}) in his Analysis
+  Webnotes available at \url{http://www.math.unl.edu/~webnotes}.
+
+  Lemmas about sequences of reals are used to reach the result.
+*}
 
 lemma lemma_nth_realpow_non_empty:
      "[| (0::real) < a; 0 < n |] ==> \<exists>s. s : {x. x ^ n <= a & 0 < x}"