diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Isar_Ref/Preface.thy
--- a/src/Doc/Isar_Ref/Preface.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/Preface.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -20,19 +20,19 @@
   transactions with unlimited undo etc.
 
   In its pioneering times, the Isabelle/Isar version of the
-  \<^emph>\<open>Proof~General\<close> user interface @{cite proofgeneral and
-  "Aspinall:TACAS:2000"} has contributed to the
+  \<^emph>\<open>Proof~General\<close> user interface \<^cite>\<open>proofgeneral and
+  "Aspinall:TACAS:2000"\<close> has contributed to the
   success of for interactive theory and proof development in this
   advanced theorem proving environment, even though it was somewhat
   biased towards old-style proof scripts.  The more recent
-  Isabelle/jEdit Prover IDE @{cite "Wenzel:2012"} emphasizes the
+  Isabelle/jEdit Prover IDE \<^cite>\<open>"Wenzel:2012"\<close> emphasizes the
   document-oriented approach of Isabelle/Isar again more explicitly.
 
   \<^medskip>
   Apart from the technical advances over bare-bones ML
   programming, the main purpose of the Isar language is to provide a
   conceptually different view on machine-checked proofs
-  @{cite "Wenzel:1999:TPHOL" and "Wenzel-PhD"}.  \<^emph>\<open>Isar\<close> stands for
+  \<^cite>\<open>"Wenzel:1999:TPHOL" and "Wenzel-PhD"\<close>.  \<^emph>\<open>Isar\<close> stands for
   \<^emph>\<open>Intelligible semi-automated reasoning\<close>.  Drawing from both the
   traditions of informal mathematical proof texts and high-level
   programming languages, Isar offers a versatile environment for