diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Tutorial/Documents/Documents.thy
--- a/src/Doc/Tutorial/Documents/Documents.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/Documents/Documents.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -11,7 +11,7 @@
   for the parser and output templates for the pretty printer.
 
   In full generality, parser and pretty printer configuration is a
-  subtle affair~@{cite "isabelle-isar-ref"}.  Your syntax specifications need
+  subtle affair~\<^cite>\<open>"isabelle-isar-ref"\<close>.  Your syntax specifications need
   to interact properly with the existing setup of Isabelle/Pure and
   Isabelle/HOL\@.  To avoid creating ambiguities with existing
   elements, it is particularly important to give new syntactic
@@ -106,7 +106,7 @@
   display the \verb,\,\verb,<forall>, symbol as~\<open>\<forall>\<close>.
 
   A list of standard Isabelle symbols is given in
-  @{cite "isabelle-isar-ref"}.  You may introduce your own
+  \<^cite>\<open>"isabelle-isar-ref"\<close>.  You may introduce your own
   interpretation of further symbols by configuring the appropriate
   front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
   macros (see also \S\ref{sec:doc-prep-symbols}).  There are also a
@@ -146,7 +146,7 @@
 
 text \<open>
   It is possible to provide alternative syntax forms
-  through the \bfindex{print mode} concept~@{cite "isabelle-isar-ref"}.  By
+  through the \bfindex{print mode} concept~\<^cite>\<open>"isabelle-isar-ref"\<close>.  By
   convention, the mode of ``$xsymbols$'' is enabled whenever
   Proof~General's X-Symbol mode or {\LaTeX} output is active.  Now
   consider the following hybrid declaration of \<open>xor\<close>:
@@ -180,7 +180,7 @@
 
 text \<open>
   Prefix syntax annotations\index{prefix annotation} are another form
-  of mixfixes @{cite "isabelle-isar-ref"}, without any template arguments or
+  of mixfixes \<^cite>\<open>"isabelle-isar-ref"\<close>, without any template arguments or
   priorities --- just some literal syntax.  The following example
   associates common symbols with the constructors of a datatype.
 \<close>
@@ -254,7 +254,7 @@
 
 Abbreviations are a simplified form of the general concept of
 \emph{syntax translations}; even heavier transformations may be
-written in ML @{cite "isabelle-isar-ref"}.
+written in ML \<^cite>\<open>"isabelle-isar-ref"\<close>.
 \<close>
 
 
@@ -342,7 +342,7 @@
   setup) and \texttt{isabelle build} (to run sessions as specified in
   the corresponding \texttt{ROOT} file).  These Isabelle tools are
   described in further detail in the \emph{Isabelle System Manual}
-  @{cite "isabelle-system"}.
+  \<^cite>\<open>"isabelle-system"\<close>.
 
   For example, a new session \texttt{MySession} (with document
   preparation) may be produced as follows:
@@ -403,7 +403,7 @@
   \texttt{MySession/document} directory as well.  In particular,
   adding a file named \texttt{root.bib} causes an automatic run of
   \texttt{bibtex} to process a bibliographic database; see also
-  \texttt{isabelle document} @{cite "isabelle-system"}.
+  \texttt{isabelle document} \<^cite>\<open>"isabelle-system"\<close>.
 
   \medskip Any failure of the document preparation phase in an
   Isabelle batch session leaves the generated sources in their target
@@ -473,7 +473,7 @@
   theory or proof context (\bfindex{text blocks}).
 
   \medskip Marginal comments are part of each command's concrete
-  syntax @{cite "isabelle-isar-ref"}; the common form is ``\verb,--,~$text$''
+  syntax \<^cite>\<open>"isabelle-isar-ref"\<close>; the common form is ``\verb,--,~$text$''
   where $text$ is delimited by \verb,",\<open>\<dots>\<close>\verb,", or
   \verb,{,\verb,*,~\<open>\<dots>\<close>~\verb,*,\verb,}, as before.  Multiple
   marginal comments may be given at the same time.  Here is a simple
@@ -552,7 +552,7 @@
   same types as they have in the main goal statement.
 
   \medskip Several further kinds of antiquotations and options are
-  available @{cite "isabelle-isar-ref"}.  Here are a few commonly used
+  available \<^cite>\<open>"isabelle-isar-ref"\<close>.  Here are a few commonly used
   combinations:
 
   \medskip
@@ -600,7 +600,7 @@
   straightforward generalization of ASCII characters.  While Isabelle
   does not impose any interpretation of the infinite collection of
   named symbols, {\LaTeX} documents use canonical glyphs for certain
-  standard symbols @{cite "isabelle-isar-ref"}.
+  standard symbols \<^cite>\<open>"isabelle-isar-ref"\<close>.
 
   The {\LaTeX} code produced from Isabelle text follows a simple
   scheme.  You can tune the final appearance by redefining certain
@@ -690,7 +690,7 @@
   preparation system allows the user to specify how to interpret a
   tagged region, in order to keep, drop, or fold the corresponding
   parts of the document.  See the \emph{Isabelle System Manual}
-  @{cite "isabelle-system"} for further details, especially on
+  \<^cite>\<open>"isabelle-system"\<close> for further details, especially on
   \texttt{isabelle build} and \texttt{isabelle document}.
 
   Ignored material is specified by delimiting the original formal