src/HOL/GCD.thy

 lemmas are proved uniformly for the natural numbers and integers.
 
 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
 extended gcd, lcm, primes to the integers. Amine Chaieb provided
 another extension of the notions to the integers, and added a number

 text {*
   \medskip Multiplication laws
 *}
 
 lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
-    -- {* \cite[page 27]{davenport92} *}
+    -- {* @{cite \<open>page 27\<close> davenport92} *}
   apply (induct m n rule: gcd_nat_induct)
   apply simp
   apply (case_tac "k = 0")
   apply (simp_all add: gcd_non_0_nat)
 done