changeset 58623 2db1df2c8467
parent 57512 cc97b347b301
child 58645 94bef115c08f
--- 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