equal
deleted
inserted
replaced
|
1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
|
2 |
1 <!-- $Id$ --> |
3 <!-- $Id$ --> |
2 <HTML><HEAD><TITLE>HOL/Algebra/README.html</TITLE></HEAD><BODY> |
4 <HTML><HEAD><TITLE>HOL/Algebra/README.html</TITLE></HEAD><BODY> |
3 |
5 |
4 <H1>Algebra --- Classical Algebra, using Explicit Structures and Locales</H1> |
6 <H1>Algebra --- Classical Algebra, using Explicit Structures and Locales</H1> |
5 |
7 |
10 The library is expected to grow in future releases of Isabelle. |
12 The library is expected to grow in future releases of Isabelle. |
11 Contributions are welcome. |
13 Contributions are welcome. |
12 |
14 |
13 <H2>GroupTheory, including Sylow's Theorem</H2> |
15 <H2>GroupTheory, including Sylow's Theorem</H2> |
14 |
16 |
15 <P>These proofs are mainly by Florian Kammüller. (Later, Larry |
17 <P>These proofs are mainly by Florian Kammller. (Later, Larry |
16 Paulson simplified some of the proofs.) These theories were indeed |
18 Paulson simplified some of the proofs.) These theories were indeed |
17 the original motivation for locales. |
19 the original motivation for locales. |
18 |
20 |
19 Here is an outline of the directory's contents: <UL> <LI>Theory <A |
21 Here is an outline of the directory's contents: <UL> <LI>Theory <A |
20 HREF="Group.html"><CODE>Group</CODE></A> defines semigroups, monoids, |
22 HREF="Group.html"><CODE>Group</CODE></A> defines semigroups, monoids, |