src/HOL/Real/README.html
changeset 12254 78bc1f3462b5
parent 10156 9d4d5852eb47
child 14631 ec1e67f88f49
--- a/src/HOL/Real/README.html	Tue Nov 20 22:53:05 2001 +0100
+++ b/src/HOL/Real/README.html	Tue Nov 20 22:53:50 2001 +0100
@@ -3,7 +3,7 @@
 
 <H2>Real--Dedekind Cut Construction of the Real Line</H2>
 
-<UL>
+<ul>
 <LI><A HREF="PNat.html">PNat</A>  The positive integers (very much the same as <A HREF="../Nat.html">Nat.thy</A>!) 
 <LI><A HREF="PRat.html">PRat</A>  The positive rationals
 <LI><A HREF="PReal.html">PReal</A> The positive reals constructed using Dedekind cuts
@@ -22,8 +22,11 @@
 </ul>
 
 <H2>Hyperreal--Ultrapower Construction of the Non-Standard Reals</H2>
-<LI> See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard
-Real Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190.
+
+<p>
+See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard Real
+Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190.
+</p>
 
 <UL>
 <LI><A HREF="Zorn.html">Zorn</A>