src/HOL/GCD.thy

--- a/src/HOL/GCD.thy	Wed Feb 01 20:07:13 2023 +0100
+++ b/src/HOL/GCD.thy	Wed Feb 01 20:21:33 2023 +0100
@@ -2011,7 +2011,7 @@
 
 lemma gcd_mult_distrib_nat: "k * gcd m n = gcd (k * m) (k * n)"
   for k m n :: nat
-  \<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close>
+  \<comment> \<open>\<^cite>\<open>\<open>page 27\<close> in davenport92\<close>\<close>
   by (simp add: gcd_mult_left)
 
 lemma gcd_mult_distrib_int: "\<bar>k\<bar> * gcd m n = gcd (k * m) (k * n)"