--- 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