--- a/src/HOL/GroupTheory/README.html Tue Nov 20 22:53:05 2001 +0100
+++ b/src/HOL/GroupTheory/README.html Tue Nov 20 22:53:50 2001 +0100
@@ -12,29 +12,29 @@
Here is an outline of the directory's contents:
<UL>
-<LI>Theory <A HREF="Bij.thy"><CODE>Bij</CODE></A>
+<LI>Theory <A HREF="Bij.html"><CODE>Bij</CODE></A>
defines bijections over sets and operations on them and shows that they
are a group.
-<LI>Theory <A HREF="DirProd.thy"><CODE>DirProd</CODE></A>
+<LI>Theory <A HREF="DirProd.html"><CODE>DirProd</CODE></A>
defines the product of two groups and proves that it is a group again.
-<LI>Theory <A HREF="FactGroup.thy"><CODE>FactGroup</CODE></A>
+<LI>Theory <A HREF="FactGroup.html"><CODE>FactGroup</CODE></A>
defines the factorization of a group and shows that the factorization a
normal subgroup is a group.
-<LI>Theory <A HREF="Homomorphism.thy"><CODE>Homomorphism</CODE></A>
+<LI>Theory <A HREF="Homomorphism.html"><CODE>Homomorphism</CODE></A>
defines homomorphims and automorphisms for groups and rings and shows that
ring automorphisms are a group by using the previous result for
bijections.
-<LI>Theory <A HREF="Ring.thy"><CODE>Ring</CODE></A>
-and <A HREF="RingConstr.thy"><CODE>RingConstr</CODE></A>
+<LI>Theory <A HREF="Ring.html"><CODE>Ring</CODE></A>
+and <A HREF="RingConstr.html"><CODE>RingConstr</CODE></A>
defines rings, proves a few basic theorems and constructs a lambda
function to extract the group that is part of the ring showing that it is
an abelian group.
-<LI>Theory <A HREF="Sylow.thy"><CODE>Sylow</CODE></A>
+<LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A>
contains a proof of the first Sylow theorem.
</UL>
--- a/src/HOL/Hyperreal/README.html Tue Nov 20 22:53:05 2001 +0100
+++ b/src/HOL/Hyperreal/README.html Tue Nov 20 22:53:50 2001 +0100
@@ -2,9 +2,8 @@
<HTML><HEAD><TITLE>HOL/Real/README</TITLE></HEAD><BODY>
<H2>Hyperreal--Ultrafilter 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.
-<UL>
+See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard Real
+Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190.
<UL>
<LI><A HREF="Zorn.html">Zorn</A>
@@ -44,7 +43,6 @@
<LI><A HREF="Series.html">Series</A>
Standard theory of finite summation and infinite series
-
</UL>
<P>Last modified on $Date$
--- 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>