src/HOL/Algebra/Sylow.thy
changeset 58622 aa99568f56de
parent 55157 06897ea77f78
child 59807 22bc39064290
--- a/src/HOL/Algebra/Sylow.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/Algebra/Sylow.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -7,7 +7,7 @@
 begin
 
 text {*
-  See also \cite{Kammueller-Paulson:1999}.
+  See also @{cite "Kammueller-Paulson:1999"}.
 *}
 
 text{*The combinatorial argument is in theory Exponent*}