equal
deleted
inserted
replaced
1 <!-- $Id$ --> |
1 <!-- $Id$ --> |
2 <HTML><HEAD><TITLE>HOL/Algebra/README.html</TITLE></HEAD><BODY> |
2 <HTML><HEAD><TITLE>HOL/Algebra/README.html</TITLE></HEAD><BODY> |
3 |
3 |
4 <H1>Algebra --- Classical Algebra, using Explicit Structures and Locales</H1> |
4 <H1>Algebra --- Classical Algebra, using Explicit Structures and Locales</H1> |
5 |
5 |
6 This directory presents proofs in classical algebra. |
6 This directory contains proofs in classical algebra. It is intended |
|
7 as a base for any algebraic development in Isabelle. Emphasis is on |
|
8 reusability. This is achieved by modelling algebraic structures |
|
9 as first-class citizens of the logic (not axiomatic type classes, say). |
|
10 The library is expected to grow in future releases of Isabelle. |
|
11 Contributions are welcome. |
7 |
12 |
8 <H2>GroupTheory, including Sylow's Theorem</H2> |
13 <H2>GroupTheory, including Sylow's Theorem</H2> |
9 |
14 |
10 <P>These proofs are mainly by Florian Kammüller. (Later, Larry |
15 <P>These proofs are mainly by Florian Kammüller. (Later, Larry |
11 Paulson simplified some of the proofs.) These theories were indeed |
16 Paulson simplified some of the proofs.) These theories were indeed |