src/HOL/GCD.thy
changeset 58623 2db1df2c8467
parent 57514 bdc2c6b40bf2
child 58770 ae5e9b4f8daf
--- a/src/HOL/GCD.thy	Tue Oct 07 23:12:08 2014 +0200
+++ b/src/HOL/GCD.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
@@ -364,7 +364,7 @@
 *}
 
 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")