--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy Tue Oct 07 23:12:08 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy Tue Oct 07 23:29:43 2014 +0200
@@ -10,7 +10,7 @@
begin
text {*
- See \cite{davenport92}. \bigskip
+ See @{cite davenport92}. \bigskip
*}
subsection {* Specification of GCD on nats *}
@@ -130,7 +130,7 @@
*}
lemma gcd_mult_distrib2: "k * gcd m n = gcd (k * m) (k * n)"
- -- {* \cite[page 27]{davenport92} *}
+ -- {* @{cite \<open>page 27\<close> davenport92} *}
apply (induct m n rule: gcd_induct)
apply simp
apply (case_tac "k = 0")