src/HOL/GCD.thy
changeset 58623 2db1df2c8467
parent 57514 bdc2c6b40bf2
child 58770 ae5e9b4f8daf
     1.1 --- a/src/HOL/GCD.thy	Tue Oct 07 23:12:08 2014 +0200
     1.2 +++ b/src/HOL/GCD.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
    1.12 @@ -364,7 +364,7 @@
    1.13  *}
    1.14  
    1.15  lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
    1.16 -    -- {* \cite[page 27]{davenport92} *}
    1.17 +    -- {* @{cite \<open>page 27\<close> davenport92} *}
    1.18    apply (induct m n rule: gcd_nat_induct)
    1.19    apply simp
    1.20    apply (case_tac "k = 0")