changeset 35849 | b5522b51cb1e |
parent 33657 | a4179bf442d1 |
child 41541 | 1fa4725c4656 |
35848:5443079512ea | 35849:b5522b51cb1e |
---|---|
1 (* Title: HOL/Algebra/Sylow.thy |
1 (* Title: HOL/Algebra/Sylow.thy |
2 ID: $Id$ |
|
3 Author: Florian Kammueller, with new proofs by L C Paulson |
2 Author: Florian Kammueller, with new proofs by L C Paulson |
4 *) |
3 *) |
5 |
4 |
6 theory Sylow imports Coset Exponent begin |
5 theory Sylow |
6 imports Coset Exponent |
|
7 begin |
|
7 |
8 |
8 text {* |
9 text {* |
9 See also \cite{Kammueller-Paulson:1999}. |
10 See also \cite{Kammueller-Paulson:1999}. |
10 *} |
11 *} |
11 |
12 |