diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Implementation/Eq.thy
--- a/src/Doc/Implementation/Eq.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Implementation/Eq.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -74,10 +74,10 @@
 section \<open>Conversions \label{sec:conv}\<close>
 
 text \<open>
-  The classic article @{cite "paulson:1983"} introduces the concept of
+  The classic article \<^cite>\<open>"paulson:1983"\<close> introduces the concept of
   conversion for Cambridge LCF. This was historically important to implement
   all kinds of ``simplifiers'', but the Isabelle Simplifier is done quite
-  differently, see @{cite \<open>\S9.3\<close> "isabelle-isar-ref"}.
+  differently, see \<^cite>\<open>\<open>\S9.3\<close> in "isabelle-isar-ref"\<close>.
 \<close>
 
 text %mlref \<open>