--- a/src/HOL/GroupTheory/README.html Mon May 05 18:23:40 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-<!-- $Id$ -->
-<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
-
-<H2>GroupTheory -- Group Theory using Locales, including Sylow's Theorem</H2>
-
-<P>This directory presents proofs about group theory, by
-Florian Kammüller. (Later, Larry Paulson simplified some of the proofs.)
-These theories use locales and were indeed the original motivation for
-locales. However, this treatment of groups must still be regarded as
-experimental. We can expect to see refinements in the future.
-
-Here is an outline of the directory's contents:
-
-<UL> <LI>Theory <A HREF="Group.html"><CODE>Group</CODE></A> defines
-semigroups, groups, homomorphisms and the subgroup relation. It also defines
-the product of two groups. It defines the factorization of a group and shows
-that the factorization a normal subgroup is a group.
-
-<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. It shows that automorphisms form a group.
-
-<LI>Theory <A HREF="Ring.html"><CODE>Ring</CODE></A> defines rings and proves
-a few basic theorems. Ring automorphisms are shown to form a group.
-
-<LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A>
-contains a proof of the first Sylow theorem.
-
-<LI>Theory <A HREF="Summation.html"><CODE>Summation</CODE></A> Extends
-abelian groups by a summation operator for finite sets (provided by
-Clemens Ballarin).
-</UL>
-
-<HR>
-<P>Last modified on $Date$
-
-<ADDRESS>
-<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
-</ADDRESS>
-</BODY></HTML>