diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/Sylow.thy --- a/src/HOL/Algebra/Sylow.thy Sun Mar 21 16:51:37 2010 +0100 +++ b/src/HOL/Algebra/Sylow.thy Sun Mar 21 17:12:31 2010 +0100 @@ -1,9 +1,10 @@ (* Title: HOL/Algebra/Sylow.thy - ID: $Id$ Author: Florian Kammueller, with new proofs by L C Paulson *) -theory Sylow imports Coset Exponent begin +theory Sylow +imports Coset Exponent +begin text {* See also \cite{Kammueller-Paulson:1999}.