--- 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