--- a/src/HOL/GroupTheory/README.html	Tue Dec 10 10:40:32 2002 +0100
+++ b/src/HOL/GroupTheory/README.html	Wed Dec 11 10:12:48 2002 +0100
@@ -25,6 +25,10 @@
 
 <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>