--- 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>