changeset 13975 c8e9a89883ce
parent 13949 0ce528cd6f19
child 15283 f21466450330
--- 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>