summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Algebra/README.html

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>