diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Locales/Examples3.thy
--- a/src/Doc/Locales/Examples3.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Locales/Examples3.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -486,13 +486,13 @@
 
 text \<open>More information on locales and their interpretation is
   available.  For the locale hierarchy of import and interpretation
-  dependencies see~@{cite Ballarin2006a}; interpretations in theories
-  and proofs are covered in~@{cite Ballarin2006b}.  In the latter, I
+  dependencies see~\<^cite>\<open>Ballarin2006a\<close>; interpretations in theories
+  and proofs are covered in~\<^cite>\<open>Ballarin2006b\<close>.  In the latter, I
   show how interpretation in proofs enables to reason about families
   of algebraic structures, which cannot be expressed with locales
   directly.
 
-  Haftmann and Wenzel~@{cite HaftmannWenzel2007} overcome a restriction
+  Haftmann and Wenzel~\<^cite>\<open>HaftmannWenzel2007\<close> overcome a restriction
   of axiomatic type classes through a combination with locale
   interpretation.  The result is a Haskell-style class system with a
   facility to generate ML and Haskell code.  Classes are sufficient for
@@ -504,14 +504,14 @@
   The locales reimplementation for Isabelle 2009 provides, among other
   improvements, a clean integration with Isabelle/Isar's local theory
   mechanisms, which are described in another paper by Haftmann and
-  Wenzel~@{cite HaftmannWenzel2009}.
+  Wenzel~\<^cite>\<open>HaftmannWenzel2009\<close>.
 
-  The original work of Kammüller on locales~@{cite KammullerEtAl1999}
+  The original work of Kammüller on locales~\<^cite>\<open>KammullerEtAl1999\<close>
   may be of interest from a historical perspective.  My previous
-  report on locales and locale expressions~@{cite Ballarin2004a}
+  report on locales and locale expressions~\<^cite>\<open>Ballarin2004a\<close>
   describes a simpler form of expressions than available now and is
   outdated. The mathematical background on orders and lattices is
-  taken from Jacobson's textbook on algebra~@{cite \<open>Chapter~8\<close> Jacobson1985}.
+  taken from Jacobson's textbook on algebra~\<^cite>\<open>\<open>Chapter~8\<close> in Jacobson1985\<close>.
 
   The sources of this tutorial, which include all proofs, are
   available with the Isabelle distribution at