src/HOL/Algebra/README.html

 <P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.
 
 <P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
   Author's <A HREF="http://iaks-www.ira.uka.de/iaks-calmet/ballarin/publications.html">PhD thesis</A>, 1999.
 
+<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>
 <P><A HREF="http://iaks-www.ira.uka.de/iaks-calmet/ballarin">Clemens Ballarin</A>.  Karlsruhe, October 1999