--- a/src/HOL/Algebra/Sylow.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Algebra/Sylow.thy Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
header {* Sylow's theorem *}
-theory Sylow = Coset:
+theory Sylow imports Coset begin
text {*
See also \cite{Kammueller-Paulson:1999}.