--- a/src/HOL/Algebra/README.html Wed May 07 17:46:04 2003 +0200
+++ b/src/HOL/Algebra/README.html Wed May 07 22:07:33 2003 +0200
@@ -3,7 +3,12 @@
<H1>Algebra --- Classical Algebra, using Explicit Structures and Locales</H1>
-This directory presents proofs in classical algebra.
+This directory contains proofs in classical algebra. It is intended
+as a base for any algebraic development in Isabelle. Emphasis is on
+reusability. This is achieved by modelling algebraic structures
+as first-class citizens of the logic (not axiomatic type classes, say).
+The library is expected to grow in future releases of Isabelle.
+Contributions are welcome.
<H2>GroupTheory, including Sylow's Theorem</H2>