src/HOL/Number_Theory/Primes.thy
changeset 58623 2db1df2c8467
parent 57512 cc97b347b301
child 58645 94bef115c08f
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Tue Oct 07 23:12:08 2014 +0200
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Tue Oct 07 23:29:43 2014 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  This file combines and revises a number of prior developments.
     1.5  
     1.6  The original theories "GCD" and "Primes" were by Christophe Tabacznyj
     1.7 -and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
     1.8 +and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
     1.9  gcd, lcm, and prime for the natural numbers.
    1.10  
    1.11  The original theory "IntPrimes" was by Thomas M. Rasmussen, and