isabelle: src/HOL/GroupTheory/README.html@7e6cdcd113a2 (annotated)

11443 77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	1	<!-- $Id$ -->
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	2	<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	3
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	4	<H2>GroupTheory -- Group Theory using Locales, including Sylow's Theorem</H2>
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	5
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	6	<P>This directory presents proofs about group theory, by
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	7	Florian Kamm�ller. (Later, Larry Paulson simplified some of the proofs.)
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	8	These theories use locales and were indeed the original motivation for
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	9	locales. However, this treatment of groups must still be regarded as
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	10	experimental. We can expect to see refinements in the future.
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	11
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	12	Here is an outline of the directory's contents:
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	13
13583 5fcc8bf538ee converted to Isar and using new "implicit structures" instead of Sigma, etc paulson parents: 12254 diff changeset	14	<UL> <LI>Theory <A HREF="Group.html"><CODE>Group</CODE></A> defines
5fcc8bf538ee converted to Isar and using new "implicit structures" instead of Sigma, etc paulson parents: 12254 diff changeset	15	semigroups, groups, homomorphisms and the subgroup relation. It also defines
5fcc8bf538ee converted to Isar and using new "implicit structures" instead of Sigma, etc paulson parents: 12254 diff changeset	16	the product of two groups. It defines the factorization of a group and shows
5fcc8bf538ee converted to Isar and using new "implicit structures" instead of Sigma, etc paulson parents: 12254 diff changeset	17	that the factorization a normal subgroup is a group.
5fcc8bf538ee converted to Isar and using new "implicit structures" instead of Sigma, etc paulson parents: 12254 diff changeset	18
12254 78bc1f3462b5 fixed links etc.; wenzelm parents: 11443 diff changeset	19	<LI>Theory <A HREF="Bij.html"><CODE>Bij</CODE></A>
11443 77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	20	defines bijections over sets and operations on them and shows that they
13583 5fcc8bf538ee converted to Isar and using new "implicit structures" instead of Sigma, etc paulson parents: 12254 diff changeset	21	are a group. It shows that automorphisms form a group.
11443 77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	22
13583 5fcc8bf538ee converted to Isar and using new "implicit structures" instead of Sigma, etc paulson parents: 12254 diff changeset	23	<LI>Theory <A HREF="Ring.html"><CODE>Ring</CODE></A> defines rings and proves
5fcc8bf538ee converted to Isar and using new "implicit structures" instead of Sigma, etc paulson parents: 12254 diff changeset	24	a few basic theorems. Ring automorphisms are shown to form a group.
11443 77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	25
12254 78bc1f3462b5 fixed links etc.; wenzelm parents: 11443 diff changeset	26	<LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A>
11443 77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	27	contains a proof of the first Sylow theorem.
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	28	</UL>
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	29
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	30	<HR>
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	31	<P>Last modified on $Date$
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	32
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	33	<ADDRESS>
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	34	<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	35	</ADDRESS>
77ed7e2b56c8 The final version of Florian Kammueller's proofs paulson parents: diff changeset	36	</BODY></HTML>

author	paulson
	Fri, 27 Sep 2002 16:44:50 +0200
changeset 13595	7e6cdcd113a2
parent 13583	5fcc8bf538ee
child 13745	a31e04831dd1
permissions	-rw-r--r--