src/HOL/GroupTheory/Sylow.ML

--- a/src/HOL/GroupTheory/Sylow.ML	Mon Jul 23 13:50:23 2001 +0200
+++ b/src/HOL/GroupTheory/Sylow.ML	Mon Jul 23 17:37:29 2001 +0200
@@ -4,6 +4,11 @@
     Copyright   1998-2001  University of Cambridge
 
 Sylow's theorem using locales (combinatorial argument in Exponent.thy)
+
+See Florian Kamm\"uller and L. C. Paulson,
+    A Formal Proof of Sylow's theorem:
+	An Experiment in Abstract Algebra with Isabelle HOL
+    J. Automated Reasoning 23 (1999), 235-264
 *)
 
 Open_locale "sylow";