diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Implementation/Prelim.thy
--- a/src/Doc/Implementation/Prelim.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Implementation/Prelim.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -50,7 +50,7 @@
   For example, there would be data for canonical introduction and elimination
   rules for arbitrary operators (depending on the object-logic and
   application), which enables users to perform standard proof steps implicitly
-  (cf.\ the \<open>rule\<close> method @{cite "isabelle-isar-ref"}).
+  (cf.\ the \<open>rule\<close> method \<^cite>\<open>"isabelle-isar-ref"\<close>).
 
   \<^medskip>
   Thus Isabelle/Isar is able to bring forth more and more concepts