src/HOL/Main.thy

--- a/src/HOL/Main.thy	Tue Oct 07 23:12:08 2014 +0200
+++ b/src/HOL/Main.thy	Tue Oct 07 23:29:43 2014 +0200
@@ -10,7 +10,7 @@
   complex numbers etc.
 *}
 
-text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
+text {* See further @{cite "Nipkow-et-al:2002:tutorial"} *}
 
 no_notation
   bot ("\<bottom>") and