diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -626,7 +626,7 @@
   applied with restriction to the first subgoal, then \<open>m\<^sub>2\<close> is applied
   consecutively with restriction to each subgoal that has newly emerged due to
   \<open>m\<^sub>1\<close>. This is analogous to the tactic combinator \<^ML_infix>\<open>THEN_ALL_NEW\<close> in
-  Isabelle/ML, see also @{cite "isabelle-implementation"}. For example, \<open>(rule
+  Isabelle/ML, see also \<^cite>\<open>"isabelle-implementation"\<close>. For example, \<open>(rule
   r; blast)\<close> applies rule \<open>r\<close> and then solves all new subgoals by \<open>blast\<close>.
 
   Moreover, the explicit goal restriction operator ``\<open>[n]\<close>'' exposes only the