src/HOL/Algebra/Sylow.thy

--- a/src/HOL/Algebra/Sylow.thy	Fri Aug 01 17:41:37 2008 +0200
+++ b/src/HOL/Algebra/Sylow.thy	Fri Aug 01 18:10:52 2008 +0200
@@ -3,10 +3,7 @@
     Author:     Florian Kammueller, with new proofs by L C Paulson
 *)
 
-theory Sylow imports Coset begin
-
-
-section {* Sylow's Theorem *}
+theory Sylow imports Coset Exponent begin
 
 text {*
   See also \cite{Kammueller-Paulson:1999}.