Added Presburger theory.
<!-- $Id$ -->
<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
<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$
<ADDRESS>
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
</ADDRESS>
</BODY></HTML>