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

src/HOL/Algebra/README.html

changeset 13944 | 9b34607cd83e |

parent 7998 | 3d0c34795831 |

child 13949 | 0ce528cd6f19 |

--- a/src/HOL/Algebra/README.html Thu May 01 10:29:44 2003 +0200 +++ b/src/HOL/Algebra/README.html Thu May 01 11:54:18 2003 +0200 @@ -48,6 +48,36 @@ <P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving, Author's <A HREF="http://iaks-www.ira.uka.de/iaks-calmet/ballarin/publications.html">PhD thesis</A>, 1999. +<H2>GroupTheory -- Group Theory using Locales, including Sylow's Theorem</H2> + +<P>This directory presents proofs about group theory, by +Florian Kammüller. (Later, Larry Paulson simplified some of the proofs.) +These theories use locales and were indeed the original motivation for +locales. However, this treatment of groups must still be regarded as +experimental. We can expect to see refinements in the future. + +Here is an outline of the directory's contents: + +<UL> <LI>Theory <A HREF="Group.html"><CODE>Group</CODE></A> defines +semigroups, groups, homomorphisms and the subgroup relation. It also defines +the product of two groups. It defines the factorization of a group and shows +that the factorization a normal subgroup is a group. + +<LI>Theory <A HREF="Bij.html"><CODE>Bij</CODE></A> +defines bijections over sets and operations on them and shows that they +are a group. It shows that automorphisms form a group. + +<LI>Theory <A HREF="Ring.html"><CODE>Ring</CODE></A> defines rings and proves +a few basic theorems. Ring automorphisms are shown to form a group. + +<LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A> +contains a proof of the first Sylow theorem. + +<LI>Theory <A HREF="Summation.html"><CODE>Summation</CODE></A> Extends +abelian groups by a summation operator for finite sets (provided by +Clemens Ballarin). +</UL> + <HR> <P>Last modified on $Date$