equal
deleted
inserted
replaced
1 (* Title: HOL/Algebra/Sylow.thy |
1 (* Title: HOL/Algebra/Sylow.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Florian Kammueller, with new proofs by L C Paulson |
3 Author: Florian Kammueller, with new proofs by L C Paulson |
4 *) |
4 *) |
5 |
5 |
6 theory Sylow imports Coset begin |
6 theory Sylow imports Coset Exponent begin |
7 |
|
8 |
|
9 section {* Sylow's Theorem *} |
|
10 |
7 |
11 text {* |
8 text {* |
12 See also \cite{Kammueller-Paulson:1999}. |
9 See also \cite{Kammueller-Paulson:1999}. |
13 *} |
10 *} |
14 |
11 |