
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}.




