--- a/src/HOL/Number_Theory/Primes.thy Tue Oct 07 23:12:08 2014 +0200
+++ b/src/HOL/Number_Theory/Primes.thy Tue Oct 07 23:29:43 2014 +0200
@@ -8,7 +8,7 @@
This file combines and revises a number of prior developments.
The original theories "GCD" and "Primes" were by Christophe Tabacznyj
-and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
+and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
gcd, lcm, and prime for the natural numbers.
The original theory "IntPrimes" was by Thomas M. Rasmussen, and