# HG changeset patch
# User wenzelm
# Date 1673803818 -3600
# Node ID 4c275405faae4bb504f0ea84654de7cd6b08dabe
# Parent  1e31ddcab458785aa9ad39fcef387ad342ce8813
isabelle update -u cite;

diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Classes/Classes.thy
--- a/src/Doc/Classes/Classes.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Classes/Classes.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -5,7 +5,7 @@
 section \<open>Introduction\<close>
 
 text \<open>
-  Type classes were introduced by Wadler and Blott @{cite wadler89how}
+  Type classes were introduced by Wadler and Blott \<^cite>\<open>wadler89how\<close>
   into the Haskell language to allow for a reasonable implementation
   of overloading\footnote{throughout this tutorial, we are referring
   to classical Haskell 1.0 type classes, not considering later
@@ -43,7 +43,7 @@
 
   Indeed, type classes not only allow for simple overloading but form
   a generic calculus, an instance of order-sorted algebra
-  @{cite "nipkow-sorts93" and "Nipkow-Prehofer:1993" and "Wenzel:1997:TPHOL"}.
+  \<^cite>\<open>"nipkow-sorts93" and "Nipkow-Prehofer:1993" and "Wenzel:1997:TPHOL"\<close>.
 
   From a software engineering point of view, type classes roughly
   correspond to interfaces in object-oriented languages like Java; so,
@@ -67,7 +67,7 @@
 
   \<^noindent> From a theoretical point of view, type classes are
   lightweight modules; Haskell type classes may be emulated by SML
-  functors @{cite classes_modules}.  Isabelle/Isar offers a discipline
+  functors \<^cite>\<open>classes_modules\<close>.  Isabelle/Isar offers a discipline
   of type classes which brings all those aspects together:
 
   \begin{enumerate}
@@ -77,17 +77,17 @@
        type
     \item in connection with a ``less ad-hoc'' approach to overloading,
     \item with a direct link to the Isabelle module system:
-      locales @{cite "kammueller-locales"}.
+      locales \<^cite>\<open>"kammueller-locales"\<close>.
   \end{enumerate}
 
   \<^noindent> Isar type classes also directly support code generation in
   a Haskell like fashion. Internally, they are mapped to more
-  primitive Isabelle concepts @{cite "Haftmann-Wenzel:2006:classes"}.
+  primitive Isabelle concepts \<^cite>\<open>"Haftmann-Wenzel:2006:classes"\<close>.
 
   This tutorial demonstrates common elements of structured
   specifications and abstract reasoning with type classes by the
   algebraic hierarchy of semigroups, monoids and groups.  Our
-  background theory is that of Isabelle/HOL @{cite "isa-tutorial"}, for
+  background theory is that of Isabelle/HOL \<^cite>\<open>"isa-tutorial"\<close>, for
   which some familiarity is assumed.
 \<close>
 
@@ -418,7 +418,7 @@
   \<^noindent> As you can see from this example, for local definitions
   you may use any specification tool which works together with
   locales, such as Krauss's recursive function package
-  @{cite krauss2006}.
+  \<^cite>\<open>krauss2006\<close>.
 \<close>
 
 
@@ -576,7 +576,7 @@
   overloading, it is obvious that overloading stemming from @{command
   class} statements and @{command instantiation} targets naturally
   maps to Haskell type classes.  The code generator framework
-  @{cite "isabelle-codegen"} takes this into account.  If the target
+  \<^cite>\<open>"isabelle-codegen"\<close> takes this into account.  If the target
   language (e.g.~SML) lacks type classes, then they are implemented by
   an explicit dictionary construction.  As example, let's go back to
   the power function:
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Codegen/Computations.thy
--- a/src/Doc/Codegen/Computations.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Codegen/Computations.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -263,7 +263,7 @@
 text \<open>
   Computations are a device to implement fast proof procedures.
   Then results of a computation are often assumed to be trustable
-  and thus wrapped in oracles (see @{cite "isabelle-isar-ref"}),
+  and thus wrapped in oracles (see \<^cite>\<open>"isabelle-isar-ref"\<close>),
   as in the following example:\footnote{
   The technical details how numerals are dealt with are given later in
   \secref{sec:literal_input}.}
@@ -295,7 +295,7 @@
 text \<open>
     \<^item> Antiquotation @{ML_antiquotation computation_conv} basically yields
       a conversion of type \<^ML_type>\<open>Proof.context -> cterm -> thm\<close>
-      (see further @{cite "isabelle-implementation"}).
+      (see further \<^cite>\<open>"isabelle-implementation"\<close>).
 
     \<^item> The antiquotation expects one functional argument to bridge the
       \qt{untrusted gap};  this can be done e.g.~using an oracle.  Since that oracle
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Codegen/Evaluation.thy
--- a/src/Doc/Codegen/Evaluation.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Codegen/Evaluation.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -57,7 +57,7 @@
 subsubsection \<open>Normalization by evaluation (\<open>nbe\<close>)\<close>
 
 text \<open>
-  Normalization by evaluation @{cite "Aehlig-Haftmann-Nipkow:2008:nbe"}
+  Normalization by evaluation \<^cite>\<open>"Aehlig-Haftmann-Nipkow:2008:nbe"\<close>
   provides a comparably fast partially symbolic evaluation which
   permits also normalization of functions and uninterpreted symbols;
   the stack of code to be trusted is considerable.
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Codegen/Further.thy
--- a/src/Doc/Codegen/Further.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Codegen/Further.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -174,7 +174,7 @@
   can be generated.  But this not the case: internally, the term
   \<open>fun_power.powers\<close> is an abbreviation for the foundational
   term @{term [source] "power.powers (\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"}
-  (see @{cite "isabelle-locale"} for the details behind).
+  (see \<^cite>\<open>"isabelle-locale"\<close> for the details behind).
 
   Fortunately, a succint solution is available: a dedicated
   rewrite definition:
@@ -212,7 +212,7 @@
   If you consider imperative data structures as inevitable for a
   specific application, you should consider \emph{Imperative
   Functional Programming with Isabelle/HOL}
-  @{cite "bulwahn-et-al:2008:imperative"}; the framework described there
+  \<^cite>\<open>"bulwahn-et-al:2008:imperative"\<close>; the framework described there
   is available in session \<open>Imperative_HOL\<close>, together with a
   short primer document.
 \<close>
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Codegen/Inductive_Predicate.thy
--- a/src/Doc/Codegen/Inductive_Predicate.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Codegen/Inductive_Predicate.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -23,7 +23,7 @@
   which turns inductive specifications into equational ones, from
   which in turn executable code can be generated.  The mechanisms of
   this compiler are described in detail in
-  @{cite "Berghofer-Bulwahn-Haftmann:2009:TPHOL"}.
+  \<^cite>\<open>"Berghofer-Bulwahn-Haftmann:2009:TPHOL"\<close>.
 
   Consider the simple predicate \<^const>\<open>append\<close> given by these two
   introduction rules:
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Codegen/Introduction.thy
--- a/src/Doc/Codegen/Introduction.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Codegen/Introduction.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -11,12 +11,12 @@
 text \<open>
   This tutorial introduces the code generator facilities of \<open>Isabelle/HOL\<close>.  It allows to turn (a certain class of) HOL
   specifications into corresponding executable code in the programming
-  languages \<open>SML\<close> @{cite SML}, \<open>OCaml\<close> @{cite OCaml},
-  \<open>Haskell\<close> @{cite "haskell-revised-report"} and \<open>Scala\<close>
-  @{cite "scala-overview-tech-report"}.
+  languages \<open>SML\<close> \<^cite>\<open>SML\<close>, \<open>OCaml\<close> \<^cite>\<open>OCaml\<close>,
+  \<open>Haskell\<close> \<^cite>\<open>"haskell-revised-report"\<close> and \<open>Scala\<close>
+  \<^cite>\<open>"scala-overview-tech-report"\<close>.
 
   To profit from this tutorial, some familiarity and experience with
-  Isabelle/HOL @{cite "isa-tutorial"} and its basic theories is assumed.
+  Isabelle/HOL \<^cite>\<open>"isa-tutorial"\<close> and its basic theories is assumed.
 \<close>
 
 
@@ -31,7 +31,7 @@
   a generated program as an implementation of a higher-order rewrite
   system, then every rewrite step performed by the program can be
   simulated in the logic, which guarantees partial correctness
-  @{cite "Haftmann-Nipkow:2010:code"}.
+  \<^cite>\<open>"Haftmann-Nipkow:2010:code"\<close>.
 \<close>
 
 
@@ -235,11 +235,11 @@
     \item You may want to skim over the more technical sections
       \secref{sec:adaptation} and \secref{sec:further}.
 
-    \item The target language Scala @{cite "scala-overview-tech-report"}
+    \item The target language Scala \<^cite>\<open>"scala-overview-tech-report"\<close>
       comes with some specialities discussed in \secref{sec:scala}.
 
     \item For exhaustive syntax diagrams etc. you should visit the
-      Isabelle/Isar Reference Manual @{cite "isabelle-isar-ref"}.
+      Isabelle/Isar Reference Manual \<^cite>\<open>"isabelle-isar-ref"\<close>.
 
   \end{itemize}
 
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Codegen/Partial_Functions.thy
--- a/src/Doc/Codegen/Partial_Functions.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Codegen/Partial_Functions.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -130,7 +130,7 @@
 Type \<open>dlist\<close> in Section~\ref{sec:partiality} is defined in the same manner.
 
 The following command sets up infrastructure for lifting functions on @{typ "nat list"}
-to @{typ acyc} (used by @{command_def lift_definition} below) \cite{isabelle-isar-ref}.\<close>
+to @{typ acyc} (used by @{command_def lift_definition} below) \<^cite>\<open>"isabelle-isar-ref"\<close>.\<close>
 
 setup_lifting type_definition_acyc
 
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Codegen/Refinement.thy
--- a/src/Doc/Codegen/Refinement.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Codegen/Refinement.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -265,7 +265,7 @@
 \<close>
 
 text \<open>
-  See further @{cite "Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement"}
+  See further \<^cite>\<open>"Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement"\<close>
   for the meta theory of datatype refinement involving invariants.
 
   Typical data structures implemented by representations involving
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Corec/Corec.thy
--- a/src/Doc/Corec/Corec.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Corec/Corec.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -17,7 +17,7 @@
   \label{sec:introduction}\<close>
 
 text \<open>
-Isabelle's (co)datatype package @{cite "isabelle-datatypes"} offers a convenient
+Isabelle's (co)datatype package \<^cite>\<open>"isabelle-datatypes"\<close> offers a convenient
 syntax for introducing codatatypes. For example, the type of (infinite) streams
 can be defined as follows (cf. \<^file>\<open>~~/src/HOL/Library/Stream.thy\<close>):
 \<close>
@@ -70,13 +70,13 @@
 terminology, corecursion and coinduction take place \emph{up to} friendly
 contexts.
 
-The package fully adheres to the LCF philosophy @{cite mgordon79}: The
+The package fully adheres to the LCF philosophy \<^cite>\<open>mgordon79\<close>: The
 characteristic theorems associated with the specified corecursive functions are
 derived rather than introduced axiomatically.
 (Exceptionally, most of the internal proof obligations are omitted if the
 \<open>quick_and_dirty\<close> option is enabled.)
 The package is described in a pair of scientific papers
-@{cite "blanchette-et-al-2015-fouco" and "blanchette-et-al-201x-amico"}. Some
+\<^cite>\<open>"blanchette-et-al-2015-fouco" and "blanchette-et-al-201x-amico"\<close>. Some
 of the text and examples below originate from there.
 
 This tutorial is organized as follows:
@@ -137,7 +137,7 @@
   \label{ssec:simple-corecursion}\<close>
 
 text \<open>
-The case studies by Rutten~@{cite rutten05} and Hinze~@{cite hinze10} on stream
+The case studies by Rutten~\<^cite>\<open>rutten05\<close> and Hinze~\<^cite>\<open>hinze10\<close> on stream
 calculi serve as our starting point. The following definition of pointwise sum
 can be performed with either \keyw{primcorec} or @{command corec}:
 \<close>
@@ -229,7 +229,7 @@
 text \<open>
 \noindent
 In general, the arguments may be any bounded natural functor (BNF)
-@{cite "isabelle-datatypes"}, with the restriction that the target codatatype
+\<^cite>\<open>"isabelle-datatypes"\<close>, with the restriction that the target codatatype
 (\<^typ>\<open>nat stream\<close>) may occur only in a \emph{live} position of the BNF. For
 this reason, the following function, on unbounded sets, cannot be registered as
 a friend:
@@ -323,7 +323,7 @@
 reaching a guarded corecursive call. Intuitively, the unguarded recursive call
 can be unfolded to arbitrary finite depth, ultimately yielding a purely
 corecursive definition. An example is the \<^term>\<open>primes\<close> function from Di
-Gianantonio and Miculan @{cite "di-gianantonio-miculan-2003"}:
+Gianantonio and Miculan \<^cite>\<open>"di-gianantonio-miculan-2003"\<close>:
 \<close>
 
     corecursive primes :: "nat \<Rightarrow> nat \<Rightarrow> nat stream" where
@@ -356,7 +356,7 @@
 There is a slight complication when \<open>m = 0 \<and> n > 1\<close>: Without the first
 disjunct in the \<open>if\<close> condition, the function could stall. (This corner
 case was overlooked in the original example
-@{cite "di-gianantonio-miculan-2003"}.)
+\<^cite>\<open>"di-gianantonio-miculan-2003"\<close>.)
 
 In the following examples, termination is discharged automatically by
 @{command corec} by invoking @{method lexicographic_order}:
@@ -640,7 +640,7 @@
 
 The syntactic entity \synt{target} can be used to specify a local context,
 \synt{fix} denotes name with an optional type signature, and \synt{prop} denotes
-a HOL proposition @{cite "isabelle-isar-ref"}.
+a HOL proposition \<^cite>\<open>"isabelle-isar-ref"\<close>.
 
 The optional target is optionally followed by a combination of the following
 options:
@@ -692,7 +692,7 @@
 
 The syntactic entity \synt{target} can be used to specify a local context,
 \synt{fix} denotes name with an optional type signature, and \synt{prop} denotes
-a HOL proposition @{cite "isabelle-isar-ref"}.
+a HOL proposition \<^cite>\<open>"isabelle-isar-ref"\<close>.
 
 The optional target is optionally followed by a combination of the following
 options:
@@ -732,7 +732,7 @@
 specified prefix.
 
 The syntactic entity \synt{name} denotes an identifier and \synt{type} denotes a
-type @{cite "isabelle-isar-ref"}.
+type \<^cite>\<open>"isabelle-isar-ref"\<close>.
 \<close>
 
 
@@ -784,7 +784,7 @@
 \item[\<open>f.\<close>\hthm{code} \<open>[code]\<close>\rm:] ~ \\
 @{thm sexp.code[no_vars]} \\
 The \<open>[code]\<close> attribute is set by the \<open>code\<close> plugin
-@{cite "isabelle-datatypes"}.
+\<^cite>\<open>"isabelle-datatypes"\<close>.
 
 \item[\<open>f.\<close>\hthm{coinduct} \<open>[consumes 1, case_names t, case_conclusion D\<^sub>1 \<dots>
   D\<^sub>n]\<close>\rm:] ~ \\
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -29,7 +29,7 @@
 text \<open>
 The 2013 edition of Isabelle introduced a definitional package for freely
 generated datatypes and codatatypes. This package replaces the earlier
-implementation due to Berghofer and Wenzel @{cite "Berghofer-Wenzel:1999:TPHOL"}.
+implementation due to Berghofer and Wenzel \<^cite>\<open>"Berghofer-Wenzel:1999:TPHOL"\<close>.
 Perhaps the main advantage of the new package is that it supports recursion
 through a large class of non-datatypes, such as finite sets:
 \<close>
@@ -85,14 +85,14 @@
 the theory \<^file>\<open>~~/src/HOL/Library/BNF_Axiomatization.thy\<close>.
 
 The package, like its predecessor, fully adheres to the LCF philosophy
-@{cite mgordon79}: The characteristic theorems associated with the specified
+\<^cite>\<open>mgordon79\<close>: The characteristic theorems associated with the specified
 (co)datatypes are derived rather than introduced axiomatically.%
 \footnote{However, some of the
 internal constructions and most of the internal proof obligations are omitted
 if the \<open>quick_and_dirty\<close> option is enabled.}
 The package is described in a number of scientific papers
-@{cite "traytel-et-al-2012" and "blanchette-et-al-2014-impl" and
-"panny-et-al-2014" and "blanchette-et-al-2015-wit"}.
+\<^cite>\<open>"traytel-et-al-2012" and "blanchette-et-al-2014-impl" and
+"panny-et-al-2014" and "blanchette-et-al-2015-wit"\<close>.
 The central notion is that of a \emph{bounded natural functor} (BNF)---a
 well-behaved type constructor for which nested (co)recursion is supported.
 
@@ -106,7 +106,7 @@
 
 \item Section \ref{sec:defining-primitively-recursive-functions}, ``Defining
 Primitively Recursive Functions,'' describes how to specify functions
-using @{command primrec}. (A separate tutorial @{cite "isabelle-function"}
+using @{command primrec}. (A separate tutorial \<^cite>\<open>"isabelle-function"\<close>
 describes the more powerful \keyw{fun} and \keyw{function} commands.)
 
 \item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,''
@@ -116,7 +116,7 @@
 ``Defining Primitively Corecursive Functions,'' describes how to specify
 functions using the @{command primcorec} and
 @{command primcorecursive} commands. (A separate tutorial
-@{cite "isabelle-corec"} describes the more powerful \keyw{corec} and
+\<^cite>\<open>"isabelle-corec"\<close> describes the more powerful \keyw{corec} and
 \keyw{corecursive} commands.)
 
 \item Section \ref{sec:registering-bounded-natural-functors}, ``Registering
@@ -493,7 +493,7 @@
 datatypes specified by their constructors.
 
 The syntactic entity \synt{target} can be used to specify a local
-context (e.g., \<open>(in linorder)\<close> @{cite "isabelle-isar-ref"}),
+context (e.g., \<open>(in linorder)\<close> \<^cite>\<open>"isabelle-isar-ref"\<close>),
 and \synt{prop} denotes a HOL proposition.
 
 The optional target is optionally followed by a combination of the following
@@ -531,7 +531,7 @@
 \noindent
 The syntactic entity \synt{name} denotes an identifier, \synt{mixfix} denotes
 the usual parenthesized mixfix notation, and \synt{typefree} denotes fixed type
-variable (\<^typ>\<open>'a\<close>, \<^typ>\<open>'b\<close>, \ldots) @{cite "isabelle-isar-ref"}.
+variable (\<^typ>\<open>'a\<close>, \<^typ>\<open>'b\<close>, \ldots) \<^cite>\<open>"isabelle-isar-ref"\<close>.
 
 The optional names preceding the type variables allow to override the default
 names of the set functions (\<open>set\<^sub>1_t\<close>, \ldots, \<open>set\<^sub>m_t\<close>). Type
@@ -566,7 +566,7 @@
 \medskip
 
 \noindent
-The syntactic entity \synt{type} denotes a HOL type @{cite "isabelle-isar-ref"}.
+The syntactic entity \synt{type} denotes a HOL type \<^cite>\<open>"isabelle-isar-ref"\<close>.
 
 In addition to the type of a constructor argument, it is possible to specify a
 name for the corresponding selector. The same selector name can be reused for
@@ -602,7 +602,7 @@
     ML \<open>Old_Datatype_Data.get_info \<^theory> \<^type_name>\<open>even_nat\<close>\<close>
 
 text \<open>
-The syntactic entity \synt{name} denotes an identifier @{cite "isabelle-isar-ref"}.
+The syntactic entity \synt{name} denotes an identifier \<^cite>\<open>"isabelle-isar-ref"\<close>.
 
 The command is sometimes useful when migrating from the old datatype package to
 the new one.
@@ -1256,7 +1256,7 @@
 command, which supports primitive recursion, or using the \keyw{fun},
 \keyw{function}, and \keyw{partial_function} commands. In this tutorial, the
 focus is on @{command primrec}; \keyw{fun} and \keyw{function} are described in
-a separate tutorial @{cite "isabelle-function"}.
+a separate tutorial \<^cite>\<open>"isabelle-function"\<close>.
 
 Because it is restricted to primitive recursion, @{command primrec} is less
 powerful than \keyw{fun} and \keyw{function}. However, there are primitively
@@ -1616,7 +1616,7 @@
 The syntactic entity \synt{target} can be used to specify a local context,
 \synt{fixes} denotes a list of names with optional type signatures,
 \synt{thmdecl} denotes an optional name for the formula that follows, and
-\synt{prop} denotes a HOL proposition @{cite "isabelle-isar-ref"}.
+\synt{prop} denotes a HOL proposition \<^cite>\<open>"isabelle-isar-ref"\<close>.
 
 The optional target is optionally followed by a combination of the following
 options:
@@ -1787,8 +1787,7 @@
 command is first illustrated through concrete examples featuring different
 flavors of corecursion. More examples can be found in the directory
 \<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>. The \emph{Archive of Formal Proofs} also
-includes some useful codatatypes, notably for lazy lists @{cite
-"lochbihler-2010"}.
+includes some useful codatatypes, notably for lazy lists \<^cite>\<open>"lochbihler-2010"\<close>.
 \<close>
 
 
@@ -2080,10 +2079,10 @@
 \keyw{prim\-corec\-ursive} commands, which support primitive corecursion.
 Other approaches include the more general \keyw{partial_function} command, the
 \keyw{corec} and \keyw{corecursive} commands, and techniques based on domains
-and topologies @{cite "lochbihler-hoelzl-2014"}. In this tutorial, the focus is
+and topologies \<^cite>\<open>"lochbihler-hoelzl-2014"\<close>. In this tutorial, the focus is
 on @{command primcorec} and @{command primcorecursive}; \keyw{corec} and
 \keyw{corecursive} are described in a separate tutorial
-@{cite "isabelle-corec"}. More examples can be found in the directories
+\<^cite>\<open>"isabelle-corec"\<close>. More examples can be found in the directories
 \<^dir>\<open>~~/src/HOL/Datatype_Examples\<close> and \<^dir>\<open>~~/src/HOL/Corec_Examples\<close>.
 
 Whereas recursive functions consume datatypes one constructor at a time,
@@ -2624,7 +2623,7 @@
 The syntactic entity \synt{target} can be used to specify a local context,
 \synt{fixes} denotes a list of names with optional type signatures,
 \synt{thmdecl} denotes an optional name for the formula that follows, and
-\synt{prop} denotes a HOL proposition @{cite "isabelle-isar-ref"}.
+\synt{prop} denotes a HOL proposition \<^cite>\<open>"isabelle-isar-ref"\<close>.
 
 The optional target is optionally followed by a combination of the following
 options:
@@ -2785,7 +2784,7 @@
 text \<open>
 Bounded natural functors (BNFs) are a semantic criterion for where
 (co)re\-cur\-sion may appear on the right-hand side of an equation
-@{cite "traytel-et-al-2012" and "blanchette-et-al-2015-wit"}.
+\<^cite>\<open>"traytel-et-al-2012" and "blanchette-et-al-2015-wit"\<close>.
 
 An $n$-ary BNF is a type constructor equipped with a map function
 (functorial action), $n$ set functions (natural transformations),
@@ -3105,7 +3104,7 @@
 
 The syntactic entity \synt{target} can be used to specify a local context,
 \synt{type} denotes a HOL type, and \synt{term} denotes a HOL term
-@{cite "isabelle-isar-ref"}.
+\<^cite>\<open>"isabelle-isar-ref"\<close>.
 
 The @{syntax plugins} option indicates which plugins should be enabled
 (\<open>only\<close>) or disabled (\<open>del\<close>). By default, all plugins are enabled.
@@ -3203,7 +3202,7 @@
 \synt{name} denotes an identifier, \synt{typefree} denotes fixed type variable
 (\<^typ>\<open>'a\<close>, \<^typ>\<open>'b\<close>, \ldots), \synt{mixfix} denotes the usual parenthesized
 mixfix notation, and \synt{types} denotes a space-separated list of types
-@{cite "isabelle-isar-ref"}.
+\<^cite>\<open>"isabelle-isar-ref"\<close>.
 
 The @{syntax plugins} option indicates which plugins should be enabled
 (\<open>only\<close>) or disabled (\<open>del\<close>). By default, all plugins are enabled.
@@ -3288,7 +3287,7 @@
 
 The syntactic entity \synt{target} can be used to specify a local context,
 \synt{name} denotes an identifier, \synt{prop} denotes a HOL proposition, and
-\synt{term} denotes a HOL term @{cite "isabelle-isar-ref"}.
+\synt{term} denotes a HOL term \<^cite>\<open>"isabelle-isar-ref"\<close>.
 
 The syntax resembles that of @{command datatype} and @{command codatatype}
 definitions (Sections
@@ -3410,7 +3409,7 @@
 text \<open>
 Beyond the standard plugins, the \emph{Archive of Formal Proofs} includes a
 \keyw{derive} command that derives class instances of datatypes
-@{cite "sternagel-thiemann-2015"}.
+\<^cite>\<open>"sternagel-thiemann-2015"\<close>.
 \<close>
 
 subsection \<open>Code Generator
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Demo_EPTCS/Document.thy
--- a/src/Doc/Demo_EPTCS/Document.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Demo_EPTCS/Document.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -23,7 +23,7 @@
 
 paragraph \<open>Another paragraph.\<close>
 
-text \<open>See also @{cite \<open>\S3\<close> "isabelle-system"}.\<close>
+text \<open>See also \<^cite>\<open>\<open>\S3\<close> in "isabelle-system"\<close>.\<close>
 
 
 section \<open>Formal proof of Cantor's theorem\<close>
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Demo_Easychair/Document.thy
--- a/src/Doc/Demo_Easychair/Document.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Demo_Easychair/Document.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -23,7 +23,7 @@
 
 paragraph \<open>Another paragraph.\<close>
 
-text \<open>See also @{cite \<open>\S3\<close> "isabelle-system"}.\<close>
+text \<open>See also \<^cite>\<open>\<open>\S3\<close> in "isabelle-system"\<close>.\<close>
 
 
 section \<open>Formal proof of Cantor's theorem\<close>
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Demo_LIPIcs/Document.thy
--- a/src/Doc/Demo_LIPIcs/Document.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Demo_LIPIcs/Document.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -23,7 +23,7 @@
 
 paragraph \<open>Another paragraph.\<close>
 
-text \<open>See also @{cite \<open>\S3\<close> "isabelle-system"}.\<close>
+text \<open>See also \<^cite>\<open>\<open>\S3\<close> in "isabelle-system"\<close>.\<close>
 
 
 section \<open>Formal proof of Cantor's theorem\<close>
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Demo_LLNCS/Document.thy
--- a/src/Doc/Demo_LLNCS/Document.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Demo_LLNCS/Document.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -23,7 +23,7 @@
 
 paragraph \<open>Another paragraph.\<close>
 
-text \<open>See also @{cite \<open>\S3\<close> "isabelle-system"}.\<close>
+text \<open>See also \<^cite>\<open>\<open>\S3\<close> in "isabelle-system"\<close>.\<close>
 
 
 section \<open>Formal proof of Cantor's theorem\<close>
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Eisbach/Manual.thy
--- a/src/Doc/Eisbach/Manual.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Eisbach/Manual.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -15,7 +15,7 @@
 
   \<^medskip>
   The syntax diagram below refers to some syntactic categories that are
-  further defined in @{cite "isabelle-isar-ref"}.
+  further defined in \<^cite>\<open>"isabelle-isar-ref"\<close>.
 
   \<^rail>\<open>
     @@{command method} name args @'=' method
@@ -281,7 +281,7 @@
 
   \<^medskip>
   The syntax diagram below refers to some syntactic categories that are
-  further defined in @{cite "isabelle-isar-ref"}.
+  further defined in \<^cite>\<open>"isabelle-isar-ref"\<close>.
 
   \<^rail>\<open>
     @@{method match} kind @'in' (pattern '\<Rightarrow>' @{syntax text} + '\<bar>')
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Eisbach/Preface.thy
--- a/src/Doc/Eisbach/Preface.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Eisbach/Preface.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -6,7 +6,7 @@
 
 text \<open>
   \<^emph>\<open>Eisbach\<close> is a collection of tools which form the basis for defining new
-  proof methods in Isabelle/Isar~@{cite "Wenzel-PhD"}. It can be thought of as
+  proof methods in Isabelle/Isar~\<^cite>\<open>"Wenzel-PhD"\<close>. It can be thought of as
   a ``proof method language'', but is more precisely an infrastructure for
   defining new proof methods out of existing ones.
 
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Functions/Functions.thy
--- a/src/Doc/Functions/Functions.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Functions/Functions.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -276,7 +276,7 @@
 text \<open>
   To see how the automatic termination proofs work, let's look at an
   example where it fails\footnote{For a detailed discussion of the
-  termination prover, see @{cite bulwahnKN07}}:
+  termination prover, see \<^cite>\<open>bulwahnKN07\<close>}:
 
 \end{isamarkuptext}  
 \cmd{fun} \<open>fails :: "nat \<Rightarrow> nat list \<Rightarrow> nat"\<close>\\%
@@ -332,7 +332,7 @@
   more powerful \<open>size_change\<close> method, which uses a variant of
   the size-change principle, together with some other
   techniques. While the details are discussed
-  elsewhere @{cite krauss_phd},
+  elsewhere \<^cite>\<open>krauss_phd\<close>,
   here are a few typical situations where
   \<open>lexicographic_order\<close> has difficulties and \<open>size_change\<close>
   may be worth a try:
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>
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Implementation/Integration.thy
--- a/src/Doc/Implementation/Integration.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Implementation/Integration.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -15,8 +15,8 @@
   stateless manner. Historically, the sequence of transitions was wrapped up
   as sequential command loop, such that commands are applied one-by-one. In
   contemporary Isabelle/Isar, processing toplevel commands usually works in
-  parallel in multi-threaded Isabelle/ML @{cite "Wenzel:2009" and
-  "Wenzel:2013:ITP"}.
+  parallel in multi-threaded Isabelle/ML \<^cite>\<open>"Wenzel:2009" and
+  "Wenzel:2013:ITP"\<close>.
 \<close>
 
 
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Implementation/Isar.thy
--- a/src/Doc/Implementation/Isar.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Implementation/Isar.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -7,7 +7,7 @@
 chapter \<open>Isar language elements\<close>
 
 text \<open>
-  The Isar proof language (see also @{cite \<open>\S2\<close> "isabelle-isar-ref"})
+  The Isar proof language (see also \<^cite>\<open>\<open>\S2\<close> in "isabelle-isar-ref"\<close>)
   consists of three main categories of language elements:
 
   \<^enum> Proof \<^emph>\<open>commands\<close> define the primary language of transactions of the
@@ -86,7 +86,7 @@
   \<^descr> \<^ML>\<open>Proof.assert_forward\<close>, \<^ML>\<open>Proof.assert_chain\<close>, \<^ML>\<open>Proof.assert_backward\<close> are partial identity functions that fail unless a
   certain linguistic mode is active, namely ``\<open>proof(state)\<close>'',
   ``\<open>proof(chain)\<close>'', ``\<open>proof(prove)\<close>'', respectively (using the terminology
-  of @{cite "isabelle-isar-ref"}).
+  of \<^cite>\<open>"isabelle-isar-ref"\<close>).
 
   It is advisable study the implementations of existing proof commands for
   suitable modes to be asserted.
@@ -308,7 +308,7 @@
 \<close>
 
 text %mlex \<open>
-  See also @{command method_setup} in @{cite "isabelle-isar-ref"} which
+  See also @{command method_setup} in \<^cite>\<open>"isabelle-isar-ref"\<close> which
   includes some abstract examples.
 
   \<^medskip>
@@ -358,7 +358,7 @@
 
   The \<^ML>\<open>Attrib.thms\<close> parser produces a list of theorems from the usual Isar
   syntax involving attribute expressions etc.\ (syntax category @{syntax
-  thms}) @{cite "isabelle-isar-ref"}. The resulting \<^ML_text>\<open>thms\<close> are
+  thms}) \<^cite>\<open>"isabelle-isar-ref"\<close>. The resulting \<^ML_text>\<open>thms\<close> are
   added to \<^ML>\<open>HOL_basic_ss\<close> which already contains the basic Simplifier
   setup for HOL.
 
@@ -540,7 +540,7 @@
 \<close>
 
 text %mlex \<open>
-  See also @{command attribute_setup} in @{cite "isabelle-isar-ref"} which
+  See also @{command attribute_setup} in \<^cite>\<open>"isabelle-isar-ref"\<close> which
   includes some abstract examples.
 \<close>
 
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Implementation/Local_Theory.thy
--- a/src/Doc/Implementation/Local_Theory.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Implementation/Local_Theory.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -84,8 +84,8 @@
   When a definitional package is finished, the auxiliary context is reset to
   the target context. The target now holds definitions for terms and theorems
   that stem from the hypothetical \<open>\<DEFINE>\<close> and \<open>\<NOTE>\<close> elements,
-  transformed by the particular target policy (see @{cite \<open>\S4--5\<close>
-  "Haftmann-Wenzel:2009"} for details).
+  transformed by the particular target policy (see \<^cite>\<open>\<open>\S4--5\<close> in
+  "Haftmann-Wenzel:2009"\<close> for details).
 \<close>
 
 text %mlref \<open>
@@ -143,7 +143,7 @@
 text \<open>
   %FIXME
 
-  See also @{cite "Chaieb-Wenzel:2007"}.
+  See also \<^cite>\<open>"Chaieb-Wenzel:2007"\<close>.
 \<close>
 
 end
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Implementation/Logic.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -8,9 +8,9 @@
 
 text \<open>
   The logical foundations of Isabelle/Isar are that of the Pure logic, which
-  has been introduced as a Natural Deduction framework in @{cite paulson700}.
+  has been introduced as a Natural Deduction framework in \<^cite>\<open>paulson700\<close>.
   This is essentially the same logic as ``\<open>\<lambda>HOL\<close>'' in the more abstract
-  setting of Pure Type Systems (PTS) @{cite "Barendregt-Geuvers:2001"},
+  setting of Pure Type Systems (PTS) \<^cite>\<open>"Barendregt-Geuvers:2001"\<close>,
   although there are some key differences in the specific treatment of simple
   types in Isabelle/Pure.
 
@@ -97,7 +97,7 @@
   sorts \<open>(s\<^sub>1, \<dots>, s\<^sub>k)\<close> such that a type scheme \<open>(\<alpha>\<^bsub>s\<^sub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^sub>k\<^esub>)\<kappa>\<close> is of
   sort \<open>s\<close>. Consequently, type unification has most general solutions (modulo
   equivalence of sorts), so type-inference produces primary types as expected
-  @{cite "nipkow-prehofer"}.
+  \<^cite>\<open>"nipkow-prehofer"\<close>.
 \<close>
 
 text %mlref \<open>
@@ -255,8 +255,7 @@
 
 text \<open>
   The language of terms is that of simply-typed \<open>\<lambda>\<close>-calculus with de-Bruijn
-  indices for bound variables (cf.\ @{cite debruijn72} or @{cite
-  "paulson-ml2"}), with the types being determined by the corresponding
+  indices for bound variables (cf.\ \<^cite>\<open>debruijn72\<close> or \<^cite>\<open>"paulson-ml2"\<close>), with the types being determined by the corresponding
   binders. In contrast, free variables and constants have an explicit name and
   type in each occurrence.
 
@@ -598,15 +597,13 @@
   occur within propositions. The system provides a runtime option to record
   explicit proof terms for primitive inferences, see also
   \secref{sec:proof-terms}. Thus all three levels of \<open>\<lambda>\<close>-calculus become
-  explicit: \<open>\<Rightarrow>\<close> for terms, and \<open>\<And>/\<Longrightarrow>\<close> for proofs (cf.\ @{cite
-  "Berghofer-Nipkow:2000:TPHOL"}).
+  explicit: \<open>\<Rightarrow>\<close> for terms, and \<open>\<And>/\<Longrightarrow>\<close> for proofs (cf.\ \<^cite>\<open>"Berghofer-Nipkow:2000:TPHOL"\<close>).
 
   Observe that locally fixed parameters (as in \<open>\<And>\<hyphen>intro\<close>) need not be recorded
   in the hypotheses, because the simple syntactic types of Pure are always
   inhabitable. ``Assumptions'' \<open>x :: \<tau>\<close> for type-membership are only present
   as long as some \<open>x\<^sub>\<tau>\<close> occurs in the statement body.\<^footnote>\<open>This is the key
-  difference to ``\<open>\<lambda>HOL\<close>'' in the PTS framework @{cite
-  "Barendregt-Geuvers:2001"}, where hypotheses \<open>x : A\<close> are treated uniformly
+  difference to ``\<open>\<lambda>HOL\<close>'' in the PTS framework \<^cite>\<open>"Barendregt-Geuvers:2001"\<close>, where hypotheses \<open>x : A\<close> are treated uniformly
   for propositions and types.\<close>
 
   \<^medskip>
@@ -665,8 +662,8 @@
   previously defined constants as above, or arbitrary constants \<open>d(\<alpha>\<^sub>i)\<close> for
   some \<open>\<alpha>\<^sub>i\<close> projected from \<open>\<^vec>\<alpha>\<close>. Thus overloaded definitions
   essentially work by primitive recursion over the syntactic structure of a
-  single type argument. See also @{cite \<open>\S4.3\<close>
-  "Haftmann-Wenzel:2006:classes"}.
+  single type argument. See also \<^cite>\<open>\<open>\S4.3\<close> in
+  "Haftmann-Wenzel:2006:classes"\<close>.
 \<close>
 
 text %mlref \<open>
@@ -1000,8 +997,8 @@
 
 text \<open>
   The idea of object-level rules is to model Natural Deduction inferences in
-  the style of Gentzen @{cite "Gentzen:1935"}, but we allow arbitrary nesting
-  similar to @{cite "Schroeder-Heister:1984"}. The most basic rule format is
+  the style of Gentzen \<^cite>\<open>"Gentzen:1935"\<close>, but we allow arbitrary nesting
+  similar to \<^cite>\<open>"Schroeder-Heister:1984"\<close>. The most basic rule format is
   that of a \<^emph>\<open>Horn Clause\<close>:
   \[
   \infer{\<open>A\<close>}{\<open>A\<^sub>1\<close> & \<open>\<dots>\<close> & \<open>A\<^sub>n\<close>}
@@ -1022,7 +1019,7 @@
 
   Nesting of rules means that the positions of \<open>A\<^sub>i\<close> may again hold compound
   rules, not just atomic propositions. Propositions of this format are called
-  \<^emph>\<open>Hereditary Harrop Formulae\<close> in the literature @{cite "Miller:1991"}. Here
+  \<^emph>\<open>Hereditary Harrop Formulae\<close> in the literature \<^cite>\<open>"Miller:1991"\<close>. Here
   we give an inductive characterization as follows:
 
   \<^medskip>
@@ -1186,7 +1183,7 @@
   \<open>\<lambda>\<close>-calculus are added, which correspond to \<open>\<And>x :: \<alpha>. B x\<close> and \<open>A \<Longrightarrow> B\<close>
   according to the propositions-as-types principle. The resulting 3-level
   \<open>\<lambda>\<close>-calculus resembles ``\<open>\<lambda>HOL\<close>'' in the more abstract setting of Pure Type
-  Systems (PTS) @{cite "Barendregt-Geuvers:2001"}, if some fine points like
+  Systems (PTS) \<^cite>\<open>"Barendregt-Geuvers:2001"\<close>, if some fine points like
   schematic polymorphism and type classes are ignored.
 
   \<^medskip>
@@ -1243,8 +1240,8 @@
   abstractions, and some argument terms of applications \<open>p \<cdot> t\<close> (if possible).
 
   There are separate operations to reconstruct the full proof term later on,
-  using \<^emph>\<open>higher-order pattern unification\<close> @{cite "nipkow-patterns" and
-  "Berghofer-Nipkow:2000:TPHOL"}.
+  using \<^emph>\<open>higher-order pattern unification\<close> \<^cite>\<open>"nipkow-patterns" and
+  "Berghofer-Nipkow:2000:TPHOL"\<close>.
 
   The \<^emph>\<open>proof checker\<close> expects a fully reconstructed proof term, and can turn
   it into a theorem by replaying its primitive inferences within the kernel.
@@ -1255,7 +1252,7 @@
 
 text \<open>
   The concrete syntax of proof terms is a slight extension of the regular
-  inner syntax of Isabelle/Pure @{cite "isabelle-isar-ref"}. Its main
+  inner syntax of Isabelle/Pure \<^cite>\<open>"isabelle-isar-ref"\<close>. Its main
   syntactic category @{syntax (inner) proof} is defined as follows:
 
   \begin{center}
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Implementation/ML.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -658,7 +658,7 @@
   \<close>
 
   Here @{syntax name} and @{syntax args} are outer syntax categories, as
-  defined in @{cite "isabelle-isar-ref"}.
+  defined in \<^cite>\<open>"isabelle-isar-ref"\<close>.
 
   \<^medskip>
   A regular antiquotation \<open>@{name args}\<close> processes its arguments by the usual
@@ -966,8 +966,7 @@
   different text styles or colours. The standard output for batch sessions
   prefixes each line of warnings by \<^verbatim>\<open>###\<close> and errors by \<^verbatim>\<open>***\<close>, but leaves
   anything else unchanged. The message body may contain further markup and
-  formatting, which is routinely used in the Prover IDE @{cite
-  "isabelle-jedit"}.
+  formatting, which is routinely used in the Prover IDE \<^cite>\<open>"isabelle-jedit"\<close>.
 
   Messages are associated with the transaction context of the running Isar
   command. This enables the front-end to manage commands and resulting
@@ -1316,8 +1315,7 @@
 
   \<^descr> \<^ML>\<open>Symbol.is_letter\<close>, \<^ML>\<open>Symbol.is_digit\<close>,
   \<^ML>\<open>Symbol.is_quasi\<close>, \<^ML>\<open>Symbol.is_blank\<close> classify standard symbols
-  according to fixed syntactic conventions of Isabelle, cf.\ @{cite
-  "isabelle-isar-ref"}.
+  according to fixed syntactic conventions of Isabelle, cf.\ \<^cite>\<open>"isabelle-isar-ref"\<close>.
 
   \<^descr> Type \<^ML_type>\<open>Symbol.sym\<close> is a concrete datatype that represents the
   different kinds of symbols explicitly, with constructors
@@ -1387,7 +1385,7 @@
     \<^enum> sequence of Isabelle symbols (see also \secref{sec:symbols}), with
     \<^ML>\<open>Symbol.explode\<close> as key operation;
   
-    \<^enum> XML tree structure via YXML (see also @{cite "isabelle-system"}), with
+    \<^enum> XML tree structure via YXML (see also \<^cite>\<open>"isabelle-system"\<close>), with
     \<^ML>\<open>YXML.parse_body\<close> as key operation.
 
   Note that Isabelle/ML string literals may refer Isabelle symbols like
@@ -1675,14 +1673,14 @@
   exponential speedup of CPU performance due to ``Moore's Law'' follows
   different rules: clock frequency has reached its peak around 2005, and
   applications need to be parallelized in order to avoid a perceived loss of
-  performance. See also @{cite "Sutter:2005"}.\<close>
+  performance. See also \<^cite>\<open>"Sutter:2005"\<close>.\<close>
 
   Isabelle/Isar exploits the inherent structure of theories and proofs to
   support \<^emph>\<open>implicit parallelism\<close> to a large extent. LCF-style theorem proving
-  provides almost ideal conditions for that, see also @{cite "Wenzel:2009"}.
+  provides almost ideal conditions for that, see also \<^cite>\<open>"Wenzel:2009"\<close>.
   This means, significant parts of theory and proof checking is parallelized
   by default. In Isabelle2013, a maximum speedup-factor of 3.5 on 4 cores and
-  6.5 on 8 cores can be expected @{cite "Wenzel:2013:ITP"}.
+  6.5 on 8 cores can be expected \<^cite>\<open>"Wenzel:2013:ITP"\<close>.
 
   \<^medskip>
   ML threads lack the memory protection of separate processes, and operate
@@ -2064,7 +2062,7 @@
 text \<open>
   Futures help to organize parallel execution in a value-oriented manner, with
   \<open>fork\<close>~/ \<open>join\<close> as the main pair of operations, and some further variants;
-  see also @{cite "Wenzel:2009" and "Wenzel:2013:ITP"}. Unlike lazy values,
+  see also \<^cite>\<open>"Wenzel:2009" and "Wenzel:2013:ITP"\<close>. Unlike lazy values,
   futures are evaluated strictly and spontaneously on separate worker threads.
   Futures may be canceled, which leads to interrupts on running evaluation
   attempts, and forces structurally related futures to fail for all time;
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Implementation/Prelim.thy
--- a/src/Doc/Implementation/Prelim.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Implementation/Prelim.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -50,7 +50,7 @@
   For example, there would be data for canonical introduction and elimination
   rules for arbitrary operators (depending on the object-logic and
   application), which enables users to perform standard proof steps implicitly
-  (cf.\ the \<open>rule\<close> method @{cite "isabelle-isar-ref"}).
+  (cf.\ the \<open>rule\<close> method \<^cite>\<open>"isabelle-isar-ref"\<close>).
 
   \<^medskip>
   Thus Isabelle/Isar is able to bring forth more and more concepts
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Implementation/Proof.thy
--- a/src/Doc/Implementation/Proof.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Implementation/Proof.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -361,7 +361,7 @@
   means of a given tactic. This acts like a dual conclusion: the proof
   demonstrates that the context may be augmented by parameters and
   assumptions, without affecting any conclusions that do not mention these
-  parameters. See also @{cite "isabelle-isar-ref"} for the corresponding Isar
+  parameters. See also \<^cite>\<open>"isabelle-isar-ref"\<close> for the corresponding Isar
   proof command @{command obtain}. Final results, which may not refer to the
   parameters in the conclusion, need to exported explicitly into the original
   context.
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Implementation/Syntax.thy
--- a/src/Doc/Implementation/Syntax.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Implementation/Syntax.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -12,13 +12,13 @@
   abstract syntax\<close> --- but end-users require additional means for reading and
   printing of terms and types. This important add-on outside the logical core
   is called \<^emph>\<open>inner syntax\<close> in Isabelle jargon, as opposed to the \<^emph>\<open>outer
-  syntax\<close> of the theory and proof language @{cite "isabelle-isar-ref"}.
+  syntax\<close> of the theory and proof language \<^cite>\<open>"isabelle-isar-ref"\<close>.
 
-  For example, according to @{cite church40} quantifiers are represented as
+  For example, according to \<^cite>\<open>church40\<close> quantifiers are represented as
   higher-order constants \<open>All :: ('a \<Rightarrow> bool) \<Rightarrow> bool\<close> such that \<open>All (\<lambda>x::'a. B
   x)\<close> faithfully represents the idea that is displayed in Isabelle as \<open>\<forall>x::'a.
   B x\<close> via @{keyword "binder"} notation. Moreover, type-inference in the style
-  of Hindley-Milner @{cite hindleymilner} (and extensions) enables users to
+  of Hindley-Milner \<^cite>\<open>hindleymilner\<close> (and extensions) enables users to
   write \<open>\<forall>x. B x\<close> concisely, when the type \<open>'a\<close> is already clear from the
   context.\<^footnote>\<open>Type-inference taken to the extreme can easily confuse users.
   Beginners often stumble over unexpectedly general types inferred by the
@@ -121,8 +121,7 @@
 
   \<^medskip>
   Note that the string values that are passed in and out are annotated by the
-  system, to carry further markup that is relevant for the Prover IDE @{cite
-  "isabelle-jedit"}. User code should neither compose its own input strings,
+  system, to carry further markup that is relevant for the Prover IDE \<^cite>\<open>"isabelle-jedit"\<close>. User code should neither compose its own input strings,
   nor try to analyze the output strings. Conceptually this is an abstract
   datatype, encoded as concrete string for historical reasons.
 
@@ -150,8 +149,7 @@
   declaratively via mixfix annotations. Moreover, there are \<^emph>\<open>syntax
   translations\<close> that can be augmented by the user, either declaratively via
   @{command translations} or programmatically via @{command
-  parse_translation}, @{command print_translation} @{cite
-  "isabelle-isar-ref"}. The final scope-resolution is performed by the system,
+  parse_translation}, @{command print_translation} \<^cite>\<open>"isabelle-isar-ref"\<close>. The final scope-resolution is performed by the system,
   according to name spaces for types, term variables and constants determined
   by the context.
 \<close>
@@ -200,7 +198,7 @@
   dual, it prunes type-information before pretty printing.
 
   A typical add-on for the check/uncheck syntax layer is the @{command
-  abbreviation} mechanism @{cite "isabelle-isar-ref"}. Here the user specifies
+  abbreviation} mechanism \<^cite>\<open>"isabelle-isar-ref"\<close>. Here the user specifies
   syntactic definitions that are managed by the system as polymorphic \<open>let\<close>
   bindings. These are expanded during the \<open>check\<close> phase, and contracted during
   the \<open>uncheck\<close> phase, without affecting the type-assignment of the given
@@ -214,7 +212,7 @@
   treats certain type instances of overloaded constants according to the
   ``dictionary construction'' of its logical foundation. This involves ``type
   improvement'' (specialization of slightly too general types) and replacement
-  by certain locale parameters. See also @{cite "Haftmann-Wenzel:2009"}.
+  by certain locale parameters. See also \<^cite>\<open>"Haftmann-Wenzel:2009"\<close>.
 \<close>
 
 text %mlref \<open>
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -13,11 +13,11 @@
   sources.
 
   {\LaTeX} output is generated while processing a \<^emph>\<open>session\<close> in batch mode, as
-  explained in the \<^emph>\<open>The Isabelle System Manual\<close> @{cite "isabelle-system"}.
+  explained in the \<^emph>\<open>The Isabelle System Manual\<close> \<^cite>\<open>"isabelle-system"\<close>.
   The main Isabelle tools to get started with document preparation are
   @{tool_ref mkroot} and @{tool_ref build}.
 
-  The classic Isabelle/HOL tutorial @{cite "isabelle-hol-book"} also explains
+  The classic Isabelle/HOL tutorial \<^cite>\<open>"isabelle-hol-book"\<close> also explains
   some aspects of theory presentation.
 \<close>
 
@@ -324,8 +324,7 @@
   characters, using some type-writer font style.
 
   \<^descr> \<open>@{bash_function name}\<close> prints the given GNU bash function verbatim. The
-  name is checked wrt.\ the Isabelle system environment @{cite
-  "isabelle-system"}.
+  name is checked wrt.\ the Isabelle system environment \<^cite>\<open>"isabelle-system"\<close>.
 
   \<^descr> \<open>@{system_option name}\<close> prints the given system option verbatim. The name
   is checked wrt.\ cumulative \<^verbatim>\<open>etc/options\<close> of all Isabelle components,
@@ -605,7 +604,7 @@
     \end{tabular}
     \<^medskip>
 
-  The Isabelle document preparation system @{cite "isabelle-system"} allows
+  The Isabelle document preparation system \<^cite>\<open>"isabelle-system"\<close> allows
   tagged command regions to be presented specifically, e.g.\ to fold proof
   texts, or drop parts of the text completely.
 
@@ -627,7 +626,7 @@
   the meaning of arbitrary tags to ``keep'', ``drop'', or ``fold'' the
   corresponding parts of the text. Logic sessions may also specify ``document
   versions'', where given tags are interpreted in some particular way. Again
-  see @{cite "isabelle-system"} for further details.
+  see \<^cite>\<open>"isabelle-system"\<close> for further details.
 \<close>
 
 
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Isar_Ref/First_Order_Logic.thy
--- a/src/Doc/Isar_Ref/First_Order_Logic.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/First_Order_Logic.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -164,7 +164,7 @@
 text \<open>
   We axiomatize basic connectives of propositional logic: implication,
   disjunction, and conjunction. The associated rules are modeled after
-  Gentzen's system of Natural Deduction @{cite "Gentzen:1935"}.
+  Gentzen's system of Natural Deduction \<^cite>\<open>"Gentzen:1935"\<close>.
 \<close>
 
 axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longrightarrow>" 25)
@@ -315,7 +315,7 @@
 text \<open>
   Representing quantifiers is easy, thanks to the higher-order nature of the
   underlying framework. According to the well-known technique introduced by
-  Church @{cite "church40"}, quantifiers are operators on predicates, which
+  Church \<^cite>\<open>"church40"\<close>, quantifiers are operators on predicates, which
   are syntactically represented as \<open>\<lambda>\<close>-terms of type \<^typ>\<open>i \<Rightarrow> o\<close>. Binder
   notation turns \<open>All (\<lambda>x. B x)\<close> into \<open>\<forall>x. B x\<close> etc.
 \<close>
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Isar_Ref/Framework.thy
--- a/src/Doc/Isar_Ref/Framework.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/Framework.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -7,9 +7,9 @@
 chapter \<open>The Isabelle/Isar Framework \label{ch:isar-framework}\<close>
 
 text \<open>
-  Isabelle/Isar @{cite "Wenzel:1999:TPHOL" and "Wenzel-PhD" and
+  Isabelle/Isar \<^cite>\<open>"Wenzel:1999:TPHOL" and "Wenzel-PhD" and
   "Nipkow-TYPES02" and "Wiedijk:1999:Mizar" and "Wenzel-Paulson:2006" and
-  "Wenzel:2006:Festschrift"} is a generic framework for developing formal
+  "Wenzel:2006:Festschrift"\<close> is a generic framework for developing formal
   mathematical documents with full proof checking. Definitions, statements and
   proofs are organized as theories. A collection of theories sources may be
   presented as a printed document; see also \chref{ch:document-prep}.
@@ -32,10 +32,9 @@
   intelligible text to the human reader.
 
   The Isar proof language has emerged from careful analysis of some inherent
-  virtues of the logical framework Isabelle/Pure @{cite "paulson-found" and
-  "paulson700"}, notably composition of higher-order natural deduction rules,
-  which is a generalization of Gentzen's original calculus @{cite
-  "Gentzen:1935"}. The approach of generic inference systems in Pure is
+  virtues of the logical framework Isabelle/Pure \<^cite>\<open>"paulson-found" and
+  "paulson700"\<close>, notably composition of higher-order natural deduction rules,
+  which is a generalization of Gentzen's original calculus \<^cite>\<open>"Gentzen:1935"\<close>. The approach of generic inference systems in Pure is
   continued by Isar towards actual proof texts. See also
   \figref{fig:natural-deduction}
 
@@ -88,14 +87,13 @@
 
   \<^medskip>
   Concrete applications require another intermediate layer: an object-logic.
-  Isabelle/HOL @{cite "isa-tutorial"} (simply-typed set-theory) is most
+  Isabelle/HOL \<^cite>\<open>"isa-tutorial"\<close> (simply-typed set-theory) is most
   commonly used; elementary examples are given in the directories
   \<^dir>\<open>~~/src/Pure/Examples\<close> and \<^dir>\<open>~~/src/HOL/Examples\<close>. Some examples
   demonstrate how to start a fresh object-logic from Isabelle/Pure, and use
   Isar proofs from the very start, despite the lack of advanced proof tools at
   such an early stage (e.g.\ see
-  \<^file>\<open>~~/src/Pure/Examples/Higher_Order_Logic.thy\<close>). Isabelle/FOL @{cite
-  "isabelle-logics"} and Isabelle/ZF @{cite "isabelle-ZF"} also work, but are
+  \<^file>\<open>~~/src/Pure/Examples/Higher_Order_Logic.thy\<close>). Isabelle/FOL \<^cite>\<open>"isabelle-logics"\<close> and Isabelle/ZF \<^cite>\<open>"isabelle-ZF"\<close> also work, but are
   much less developed.
 
   In order to illustrate natural deduction in Isar, we shall subsequently
@@ -276,8 +274,8 @@
 section \<open>The Pure framework \label{sec:framework-pure}\<close>
 
 text \<open>
-  The Pure logic @{cite "paulson-found" and "paulson700"} is an intuitionistic
-  fragment of higher-order logic @{cite "church40"}. In type-theoretic
+  The Pure logic \<^cite>\<open>"paulson-found" and "paulson700"\<close> is an intuitionistic
+  fragment of higher-order logic \<^cite>\<open>"church40"\<close>. In type-theoretic
   parlance, there are three levels of \<open>\<lambda>\<close>-calculus with corresponding arrows
   \<open>\<Rightarrow>\<close>/\<open>\<And>\<close>/\<open>\<Longrightarrow>\<close>:
 
@@ -291,14 +289,13 @@
 
   Here only the types of syntactic terms, and the propositions of proof terms
   have been shown. The \<open>\<lambda>\<close>-structure of proofs can be recorded as an optional
-  feature of the Pure inference kernel @{cite "Berghofer-Nipkow:2000:TPHOL"},
+  feature of the Pure inference kernel \<^cite>\<open>"Berghofer-Nipkow:2000:TPHOL"\<close>,
   but the formal system can never depend on them due to \<^emph>\<open>proof irrelevance\<close>.
 
   On top of this most primitive layer of proofs, Pure implements a generic
-  calculus for nested natural deduction rules, similar to @{cite
-  "Schroeder-Heister:1984"}. Here object-logic inferences are internalized as
+  calculus for nested natural deduction rules, similar to \<^cite>\<open>"Schroeder-Heister:1984"\<close>. Here object-logic inferences are internalized as
   formulae over \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close>. Combining such rule statements may involve
-  higher-order unification @{cite "paulson-natural"}.
+  higher-order unification \<^cite>\<open>"paulson-natural"\<close>.
 \<close>
 
 
@@ -364,8 +361,7 @@
   connectives \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> commute. So we may assume w.l.o.g.\ that rule
   statements always observe the normal form where quantifiers are pulled in
   front of implications at each level of nesting. This means that any Pure
-  proposition may be presented as a \<^emph>\<open>Hereditary Harrop Formula\<close> @{cite
-  "Miller:1991"} which is of the form \<open>\<And>x\<^sub>1 \<dots> x\<^sub>m. H\<^sub>1 \<Longrightarrow> \<dots> H\<^sub>n \<Longrightarrow> A\<close> for \<open>m, n
+  proposition may be presented as a \<^emph>\<open>Hereditary Harrop Formula\<close> \<^cite>\<open>"Miller:1991"\<close> which is of the form \<open>\<And>x\<^sub>1 \<dots> x\<^sub>m. H\<^sub>1 \<Longrightarrow> \<dots> H\<^sub>n \<Longrightarrow> A\<close> for \<open>m, n
   \<ge> 0\<close>, and \<open>A\<close> atomic, and \<open>H\<^sub>1, \<dots>, H\<^sub>n\<close> being recursively of the same
   format. Following the convention that outermost quantifiers are implicit,
   Horn clauses \<open>A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A\<close> are a special case of this.
@@ -572,7 +568,7 @@
   may be populated later. The command \<^theory_text>\<open>method_setup\<close> allows to define proof
   methods semantically in Isabelle/ML. The Eisbach language allows to define
   proof methods symbolically, as recursive expressions over existing methods
-  @{cite "Matichuk-et-al:2014"}; see also \<^dir>\<open>~~/src/HOL/Eisbach\<close>.
+  \<^cite>\<open>"Matichuk-et-al:2014"\<close>; see also \<^dir>\<open>~~/src/HOL/Eisbach\<close>.
 
   Methods use the facts indicated by \<^theory_text>\<open>then\<close> or \<^theory_text>\<open>using\<close>, and then operate on
   the goal state. Some basic methods are predefined in Pure: ``@{method "-"}''
@@ -635,8 +631,7 @@
   \]
 
   \<^medskip>
-  The most interesting derived context element in Isar is \<^theory_text>\<open>obtain\<close> @{cite
-  \<open>\S5.3\<close> "Wenzel-PhD"}, which supports generalized elimination steps in a
+  The most interesting derived context element in Isar is \<^theory_text>\<open>obtain\<close> \<^cite>\<open>\<open>\S5.3\<close> in "Wenzel-PhD"\<close>, which supports generalized elimination steps in a
   purely forward manner. The \<^theory_text>\<open>obtain\<close> command takes a specification of
   parameters \<open>\<^vec>x\<close> and assumptions \<open>\<^vec>A\<close> to be added to the context,
   together with a proof of a case rule stating that this extension is
@@ -971,8 +966,7 @@
   etc. Due to the flexibility of rule composition
   (\secref{sec:framework-resolution}), substitution of equals by equals is
   covered as well, even substitution of inequalities involving monotonicity
-  conditions; see also @{cite \<open>\S6\<close> "Wenzel-PhD"} and @{cite
-  "Bauer-Wenzel:2001"}.
+  conditions; see also \<^cite>\<open>\<open>\S6\<close> in "Wenzel-PhD"\<close> and \<^cite>\<open>"Bauer-Wenzel:2001"\<close>.
 
   The generic calculational mechanism is based on the observation that rules
   such as \<open>trans:\<close>~\<^prop>\<open>x = y \<Longrightarrow> y = z \<Longrightarrow> x = z\<close> proceed from the premises
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -95,8 +95,7 @@
   \<^descr> @{method erule}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close>, @{method drule}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close>, and @{method
   frule}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> are similar to the basic @{method rule} method (see
   \secref{sec:pure-meth-att}), but apply rules by elim-resolution,
-  destruct-resolution, and forward-resolution, respectively @{cite
-  "isabelle-implementation"}. The optional natural number argument (default 0)
+  destruct-resolution, and forward-resolution, respectively \<^cite>\<open>"isabelle-implementation"\<close>. The optional natural number argument (default 0)
   specifies additional assumption steps to be performed here.
 
   Note that these methods are improper ones, mainly serving for
@@ -153,7 +152,7 @@
 
   \<^descr> @{attribute THEN}~\<open>a\<close> composes rules by resolution; it resolves with the
   first premise of \<open>a\<close> (an alternative position may be also specified). See
-  also \<^ML_infix>\<open>RS\<close> in @{cite "isabelle-implementation"}.
+  also \<^ML_infix>\<open>RS\<close> in \<^cite>\<open>"isabelle-implementation"\<close>.
   
   \<^descr> @{attribute unfolded}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> and @{attribute folded}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close>
   expand and fold back again the given definitions throughout a rule.
@@ -520,7 +519,7 @@
     \<open>(?x + ?y) + ?z \<equiv> ?x + (?y + ?z)\<close> \\
     \<open>f (f ?x ?y) ?z \<equiv> f ?x (f ?y ?z)\<close>
 
-    \<^enum> Higher-order patterns in the sense of @{cite "nipkow-patterns"}. These
+    \<^enum> Higher-order patterns in the sense of \<^cite>\<open>"nipkow-patterns"\<close>. These
     are terms in \<open>\<beta>\<close>-normal form (this will always be the case unless you have
     done something strange) where each occurrence of an unknown is of the form
     \<open>?F x\<^sub>1 \<dots> x\<^sub>n\<close>, where the \<open>x\<^sub>i\<close> are distinct bound variables.
@@ -701,9 +700,9 @@
 end
 
 text \<open>
-  Martin and Nipkow @{cite "martin-nipkow"} discuss the theory and give many
+  Martin and Nipkow \<^cite>\<open>"martin-nipkow"\<close> discuss the theory and give many
   examples; other algebraic structures are amenable to ordered rewriting, such
-  as Boolean rings. The Boyer-Moore theorem prover @{cite bm88book} also
+  as Boolean rings. The Boyer-Moore theorem prover \<^cite>\<open>bm88book\<close> also
   employs ordered rewriting.
 \<close>
 
@@ -756,7 +755,7 @@
   simplification procedures.
 
   \<^descr> @{attribute simp_trace_new} controls Simplifier tracing within
-  Isabelle/PIDE applications, notably Isabelle/jEdit @{cite "isabelle-jedit"}.
+  Isabelle/PIDE applications, notably Isabelle/jEdit \<^cite>\<open>"isabelle-jedit"\<close>.
   This provides a hierarchical representation of the rewriting steps performed
   by the Simplifier.
 
@@ -1115,7 +1114,7 @@
   context.  These proof procedures are slow and simplistic compared
   with high-end automated theorem provers, but they can save
   considerable time and effort in practice.  They can prove theorems
-  such as Pelletier's @{cite pelletier86} problems 40 and 41 in a few
+  such as Pelletier's \<^cite>\<open>pelletier86\<close> problems 40 and 41 in a few
   milliseconds (including full proof reconstruction):\<close>
 
 lemma "(\<exists>y. \<forall>x. F x y \<longleftrightarrow> F x x) \<longrightarrow> \<not> (\<forall>x. \<exists>y. \<forall>z. F z y \<longleftrightarrow> \<not> F z x)"
@@ -1186,8 +1185,8 @@
   desired theorem and apply rules backwards in a fairly arbitrary
   manner.  This yields a surprisingly effective proof procedure.
   Quantifiers add only few complications, since Isabelle handles
-  parameters and schematic variables.  See @{cite \<open>Chapter 10\<close>
-  "paulson-ml2"} for further discussion.\<close>
+  parameters and schematic variables.  See \<^cite>\<open>\<open>Chapter 10\<close> in
+  "paulson-ml2"\<close> for further discussion.\<close>
 
 
 subsubsection \<open>Simulating sequents by natural deduction\<close>
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -18,16 +18,16 @@
   Isabelle/HOL is based on Higher-Order Logic, a polymorphic version of
   Church's Simple Theory of Types. HOL can be best understood as a
   simply-typed version of classical set theory. The logic was first
-  implemented in Gordon's HOL system @{cite "mgordon-hol"}. It extends
-  Church's original logic @{cite "church40"} by explicit type variables (naive
+  implemented in Gordon's HOL system \<^cite>\<open>"mgordon-hol"\<close>. It extends
+  Church's original logic \<^cite>\<open>"church40"\<close> by explicit type variables (naive
   polymorphism) and a sound axiomatization scheme for new types based on
   subsets of existing types.
 
-  Andrews's book @{cite andrews86} is a full description of the original
+  Andrews's book \<^cite>\<open>andrews86\<close> is a full description of the original
   Church-style higher-order logic, with proofs of correctness and completeness
   wrt.\ certain set-theoretic interpretations. The particular extensions of
   Gordon-style HOL are explained semantically in two chapters of the 1993 HOL
-  book @{cite pitts93}.
+  book \<^cite>\<open>pitts93\<close>.
 
   Experience with HOL over decades has demonstrated that higher-order logic is
   widely applicable in many areas of mathematics and computer science. In a
@@ -238,7 +238,7 @@
 text \<open>
   Here the \<open>cases\<close> or \<open>induct\<close> rules produced by the @{command inductive}
   package coincide with the expected elimination rules for Natural Deduction.
-  Already in the original article by Gerhard Gentzen @{cite "Gentzen:1935"}
+  Already in the original article by Gerhard Gentzen \<^cite>\<open>"Gentzen:1935"\<close>
   there is a hint that each connective can be characterized by its
   introductions, and the elimination can be constructed systematically.
 \<close>
@@ -289,8 +289,7 @@
   simulating symbolic computation via rewriting.
 
   \<^descr> @{command (HOL) "function"} defines functions by general wellfounded
-  recursion. A detailed description with examples can be found in @{cite
-  "isabelle-function"}. The function is specified by a set of (possibly
+  recursion. A detailed description with examples can be found in \<^cite>\<open>"isabelle-function"\<close>. The function is specified by a set of (possibly
   conditional) recursive equations with arbitrary pattern matching. The
   command generates proof obligations for the completeness and the
   compatibility of patterns.
@@ -302,7 +301,7 @@
 
   \<^descr> @{command (HOL) "fun"} is a shorthand notation for ``@{command (HOL)
   "function"}~\<open>(sequential)\<close>'', followed by automated proof attempts regarding
-  pattern matching and termination. See @{cite "isabelle-function"} for
+  pattern matching and termination. See \<^cite>\<open>"isabelle-function"\<close> for
   further details.
 
   \<^descr> @{command (HOL) "termination"}~\<open>f\<close> commences a termination proof for the
@@ -507,7 +506,7 @@
 
   \<^descr> @{method (HOL) pat_completeness} is a specialized method to solve goals
   regarding the completeness of pattern matching, as required by the @{command
-  (HOL) "function"} package (cf.\ @{cite "isabelle-function"}).
+  (HOL) "function"} package (cf.\ \<^cite>\<open>"isabelle-function"\<close>).
 
   \<^descr> @{method (HOL) relation}~\<open>R\<close> introduces a termination proof using the
   relation \<open>R\<close>. The resulting proof state will contain goals expressing that
@@ -523,11 +522,11 @@
   @{method auto}).
 
   In case of failure, extensive information is printed, which can help to
-  analyse the situation (cf.\ @{cite "isabelle-function"}).
+  analyse the situation (cf.\ \<^cite>\<open>"isabelle-function"\<close>).
 
   \<^descr> @{method (HOL) "size_change"} also works on termination goals, using a
   variation of the size-change principle, together with a graph decomposition
-  technique (see @{cite krauss_phd} for details). Three kinds of orders are
+  technique (see \<^cite>\<open>krauss_phd\<close> for details). Three kinds of orders are
   used internally: \<open>max\<close>, \<open>min\<close>, and \<open>ms\<close> (multiset), which is only available
   when the theory \<open>Multiset\<close> is loaded. When no order kinds are given, they
   are tried in order. The search for a termination proof uses SAT solving
@@ -734,7 +733,7 @@
   These commands are mostly obsolete; @{command (HOL) "datatype"} should be
   used instead.
 
-  See @{cite "isabelle-datatypes"} for more details on datatypes. Apart from
+  See \<^cite>\<open>"isabelle-datatypes"\<close> for more details on datatypes. Apart from
   proper proof methods for case analysis and induction, there are also
   emulations of ML tactics @{method (HOL) case_tac} and @{method (HOL)
   induct_tac} available, see \secref{sec:hol-induct-tac}; these admit to refer
@@ -785,7 +784,7 @@
   infrastructure of records in Isabelle/HOL is slightly more advanced, though,
   supporting truly extensible record schemes. This admits operations that are
   polymorphic with respect to record extension, yielding ``object-oriented''
-  effects like (single) inheritance. See also @{cite "NaraschewskiW-TPHOLs98"}
+  effects like (single) inheritance. See also \<^cite>\<open>"NaraschewskiW-TPHOLs98"\<close>
   for more details on object-oriented verification and record subtyping in
   HOL.
 \<close>
@@ -841,7 +840,7 @@
   of fields as given by their declaration. The record package provides several
   standard operations like selectors and updates. The common setup for various
   generic proof tools enable succinct reasoning patterns. See also the
-  Isabelle/HOL tutorial @{cite "isabelle-hol-book"} for further instructions
+  Isabelle/HOL tutorial \<^cite>\<open>"isabelle-hol-book"\<close> for further instructions
   on using records in practice.
 \<close>
 
@@ -1041,25 +1040,25 @@
 
   To understand the concept of type definition better, we need to recount its
   somewhat complex history. The HOL logic goes back to the ``Simple Theory of
-  Types'' (STT) of A. Church @{cite "church40"}, which is further explained in
-  the book by P. Andrews @{cite "andrews86"}. The overview article by W.
-  Farmer @{cite "Farmer:2008"} points out the ``seven virtues'' of this
+  Types'' (STT) of A. Church \<^cite>\<open>"church40"\<close>, which is further explained in
+  the book by P. Andrews \<^cite>\<open>"andrews86"\<close>. The overview article by W.
+  Farmer \<^cite>\<open>"Farmer:2008"\<close> points out the ``seven virtues'' of this
   relatively simple family of logics. STT has only ground types, without
   polymorphism and without type definitions.
 
   \<^medskip>
-  M. Gordon @{cite "Gordon:1985:HOL"} augmented Church's STT by adding
+  M. Gordon \<^cite>\<open>"Gordon:1985:HOL"\<close> augmented Church's STT by adding
   schematic polymorphism (type variables and type constructors) and a facility
   to introduce new types as semantic subtypes from existing types. This
   genuine extension of the logic was explained semantically by A. Pitts in the
-  book of the original Cambridge HOL88 system @{cite "pitts93"}. Type
+  book of the original Cambridge HOL88 system \<^cite>\<open>"pitts93"\<close>. Type
   definitions work in this setting, because the general model-theory of STT is
   restricted to models that ensure that the universe of type interpretations
   is closed by forming subsets (via predicates taken from the logic).
 
   \<^medskip>
   Isabelle/HOL goes beyond Gordon-style HOL by admitting overloaded constant
-  definitions @{cite "Wenzel:1997:TPHOL" and "Haftmann-Wenzel:2006:classes"},
+  definitions \<^cite>\<open>"Wenzel:1997:TPHOL" and "Haftmann-Wenzel:2006:classes"\<close>,
   which are actually a concept of Isabelle/Pure and do not depend on
   particular set-theoretic semantics of HOL. Over many years, there was no
   formal checking of semantic type definitions in Isabelle/HOL versus
@@ -1068,11 +1067,10 @@
   \secref{sec:axiomatizations}, only with some local checks of the given type
   and its representing set.
 
-  Recent clarification of overloading in the HOL logic proper @{cite
-  "Kuncar-Popescu:2015"} demonstrates how the dissimilar concepts of constant
+  Recent clarification of overloading in the HOL logic proper \<^cite>\<open>"Kuncar-Popescu:2015"\<close> demonstrates how the dissimilar concepts of constant
   definitions versus type definitions may be understood uniformly. This
   requires an interpretation of Isabelle/HOL that substantially reforms the
-  set-theoretic model of A. Pitts @{cite "pitts93"}, by taking a schematic
+  set-theoretic model of A. Pitts \<^cite>\<open>"pitts93"\<close>, by taking a schematic
   view on polymorphism and interpreting only ground types in the set-theoretic
   sense of HOL88. Moreover, type-constructors may be explicitly overloaded,
   e.g.\ by making the subset depend on type-class parameters (cf.\
@@ -1256,8 +1254,7 @@
   package works with all four kinds of type abstraction: type copies,
   subtypes, total quotients and partial quotients.
 
-  Theoretical background can be found in @{cite
-  "Huffman-Kuncar:2013:lifting_transfer"}.
+  Theoretical background can be found in \<^cite>\<open>"Huffman-Kuncar:2013:lifting_transfer"\<close>.
 
   \begin{matharray}{rcl}
     @{command_def (HOL) "setup_lifting"} & : & \<open>local_theory \<rightarrow> local_theory\<close>\\
@@ -1459,7 +1456,7 @@
   (HOL) lifting_forget} and @{command (HOL) lifting_update} is preferred for
   normal usage.
 
-  \<^descr> Integration with the BNF package @{cite "isabelle-datatypes"}: As already
+  \<^descr> Integration with the BNF package \<^cite>\<open>"isabelle-datatypes"\<close>: As already
   mentioned, the theorems that are registered by the following attributes are
   proved and registered automatically if the involved type is BNF without dead
   variables: @{attribute (HOL) quot_map}, @{attribute (HOL) relator_eq_onp},
@@ -1545,8 +1542,7 @@
 
   Preservation of predicates on relations (\<open>bi_unique, bi_total, right_unique,
   right_total, left_unique, left_total\<close>) with the respect to a relator is
-  proved automatically if the involved type is BNF @{cite
-  "isabelle-datatypes"} without dead variables.
+  proved automatically if the involved type is BNF \<^cite>\<open>"isabelle-datatypes"\<close> without dead variables.
 
   \<^descr> @{attribute (HOL) "transfer_domain_rule"} attribute maintains a collection
   of rules, which specify a domain of a transfer relation by a predicate.
@@ -1570,8 +1566,7 @@
   is proved automatically if the involved type is BNF without dead variables.
 
 
-  Theoretical background can be found in @{cite
-  "Huffman-Kuncar:2013:lifting_transfer"}.
+  Theoretical background can be found in \<^cite>\<open>"Huffman-Kuncar:2013:lifting_transfer"\<close>.
 \<close>
 
 
@@ -1723,7 +1718,7 @@
 
   \<^descr> @{command (HOL) "sledgehammer"} attempts to prove a subgoal using external
   automatic provers (resolution provers and SMT solvers). See the Sledgehammer
-  manual @{cite "isabelle-sledgehammer"} for details.
+  manual \<^cite>\<open>"isabelle-sledgehammer"\<close> for details.
 
   \<^descr> @{command (HOL) "sledgehammer_params"} changes @{command (HOL)
   "sledgehammer"} configuration options persistently.
@@ -1876,8 +1871,7 @@
     and a lazy term reconstruction of the value in the type \<^typ>\<open>Code_Evaluation.term\<close>. A pseudo-randomness generator is defined in theory
     \<^theory>\<open>HOL.Random\<close>.
 
-    \<^descr>[\<open>narrowing\<close>] implements Haskell's Lazy Smallcheck @{cite
-    "runciman-naylor-lindblad"} using the type classes \<^class>\<open>narrowing\<close> and
+    \<^descr>[\<open>narrowing\<close>] implements Haskell's Lazy Smallcheck \<^cite>\<open>"runciman-naylor-lindblad"\<close> using the type classes \<^class>\<open>narrowing\<close> and
     \<^class>\<open>partial_term_of\<close>. Variables in the current goal are initially
     represented as symbolic variables. If the execution of the goal tries to
     evaluate one of them, the test engine replaces it with refinements
@@ -1918,7 +1912,7 @@
 
   \<^descr> @{command (HOL) "nitpick"} tests the current goal for counterexamples
   using a reduction to first-order relational logic. See the Nitpick manual
-  @{cite "isabelle-nitpick"} for details.
+  \<^cite>\<open>"isabelle-nitpick"\<close> for details.
 
   \<^descr> @{command (HOL) "nitpick_params"} changes @{command (HOL) "nitpick"}
   configuration options persistently.
@@ -1944,7 +1938,7 @@
 
   Coercive subtyping allows the user to omit explicit type conversions, also
   called \<^emph>\<open>coercions\<close>. Type inference will add them as necessary when parsing
-  a term. See @{cite "traytel-berghofer-nipkow-2011"} for details.
+  a term. See \<^cite>\<open>"traytel-berghofer-nipkow-2011"\<close> for details.
 
   \<^rail>\<open>
     @@{attribute (HOL) coercion} (@{syntax term})
@@ -2065,12 +2059,12 @@
   \<close>
 
   \<^descr> @{method (HOL) meson} implements Loveland's model elimination procedure
-  @{cite "loveland-78"}. See \<^file>\<open>~~/src/HOL/ex/Meson_Test.thy\<close> for examples.
+  \<^cite>\<open>"loveland-78"\<close>. See \<^file>\<open>~~/src/HOL/ex/Meson_Test.thy\<close> for examples.
 
   \<^descr> @{method (HOL) metis} combines ordered resolution and ordered
   paramodulation to find first-order (or mildly higher-order) proofs. The
   first optional argument specifies a type encoding; see the Sledgehammer
-  manual @{cite "isabelle-sledgehammer"} for details. The directory
+  manual \<^cite>\<open>"isabelle-sledgehammer"\<close> for details. The directory
   \<^dir>\<open>~~/src/HOL/Metis_Examples\<close> contains several small theories developed to a
   large extent using @{method (HOL) metis}.
 \<close>
@@ -2093,7 +2087,7 @@
   \<close>
 
   \<^descr> @{method (HOL) algebra} performs algebraic reasoning via Gröbner bases,
-  see also @{cite "Chaieb-Wenzel:2007"} and @{cite \<open>\S3.2\<close> "Chaieb-thesis"}.
+  see also \<^cite>\<open>"Chaieb-Wenzel:2007"\<close> and \<^cite>\<open>\<open>\S3.2\<close> in "Chaieb-thesis"\<close>.
   The method handles deals with two main classes of problems:
 
     \<^enum> Universal problems over multivariate polynomials in a
@@ -2165,8 +2159,7 @@
     @@{method (HOL) coherent} @{syntax thms}?
   \<close>
 
-  \<^descr> @{method (HOL) coherent} solves problems of \<^emph>\<open>Coherent Logic\<close> @{cite
-  "Bezem-Coquand:2005"}, which covers applications in confluence theory,
+  \<^descr> @{method (HOL) coherent} solves problems of \<^emph>\<open>Coherent Logic\<close> \<^cite>\<open>"Bezem-Coquand:2005"\<close>, which covers applications in confluence theory,
   lattice theory and projective geometry. See \<^file>\<open>~~/src/HOL/Examples/Coherent.thy\<close>
   for some examples.
 \<close>
@@ -2258,13 +2251,12 @@
   executable specifications. Isabelle/HOL instantiates these mechanisms in a
   way that is amenable to end-user applications. Code can be generated for
   functional programs (including overloading using type classes) targeting SML
-  @{cite SML}, OCaml @{cite OCaml}, Haskell @{cite "haskell-revised-report"}
-  and Scala @{cite "scala-overview-tech-report"}. Conceptually, code
+  \<^cite>\<open>SML\<close>, OCaml \<^cite>\<open>OCaml\<close>, Haskell \<^cite>\<open>"haskell-revised-report"\<close>
+  and Scala \<^cite>\<open>"scala-overview-tech-report"\<close>. Conceptually, code
   generation is split up in three steps: \<^emph>\<open>selection\<close> of code theorems,
   \<^emph>\<open>translation\<close> into an abstract executable view and \<^emph>\<open>serialization\<close> to a
   specific \<^emph>\<open>target language\<close>. Inductive specifications can be executed using
-  the predicate compiler which operates within HOL. See @{cite
-  "isabelle-codegen"} for an introduction.
+  the predicate compiler which operates within HOL. See \<^cite>\<open>"isabelle-codegen"\<close> for an introduction.
 
   \begin{matharray}{rcl}
     @{command_def (HOL) "export_code"}\<open>\<^sup>*\<close> & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -100,7 +100,7 @@
   particular print mode features. For example, @{command
   "print_state"}~\<open>(latex)\<close> prints the current proof state with mathematical
   symbols and special characters represented in {\LaTeX} source, according to
-  the Isabelle style @{cite "isabelle-system"}.
+  the Isabelle style \<^cite>\<open>"isabelle-system"\<close>.
 
   Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more systematic
   way to include formal items into the printed text document.
@@ -273,7 +273,7 @@
   to abstract syntax, and the pretty printing. Special case annotations
   provide a simple means of specifying infix operators and binders.
 
-  Isabelle mixfix syntax is inspired by {\OBJ} @{cite OBJ}. It allows to
+  Isabelle mixfix syntax is inspired by {\OBJ} \<^cite>\<open>OBJ\<close>. It allows to
   specify any context-free priority grammar, which is more general than the
   fixity declarations of ML and Prolog.
 
@@ -411,7 +411,7 @@
 
   \<^medskip>
   Note that the general idea of pretty printing with blocks and breaks is
-  described in @{cite "paulson-ml2"}; it goes back to @{cite "Oppen:1980"}.
+  described in \<^cite>\<open>"paulson-ml2"\<close>; it goes back to \<^cite>\<open>"Oppen:1980"\<close>.
 \<close>
 
 
@@ -452,7 +452,7 @@
 text \<open>
   A \<^emph>\<open>binder\<close> is a variable-binding construct such as a quantifier. The idea
   to formalize \<open>\<forall>x. b\<close> as \<open>All (\<lambda>x. b)\<close> for \<open>All :: ('a \<Rightarrow> bool) \<Rightarrow> bool\<close>
-  already goes back to @{cite church40}. Isabelle declarations of certain
+  already goes back to \<^cite>\<open>church40\<close>. Isabelle declarations of certain
   higher-order operators may be annotated with @{keyword_def "binder"}
   annotations as follows:
 
@@ -955,8 +955,7 @@
   carefully by syntax transformations.
 
   Pre-terms are further processed by the so-called \<^emph>\<open>check\<close> and \<^emph>\<open>uncheck\<close>
-  phases that are intertwined with type-inference (see also @{cite
-  "isabelle-implementation"}). The latter allows to operate on higher-order
+  phases that are intertwined with type-inference (see also \<^cite>\<open>"isabelle-implementation"\<close>). The latter allows to operate on higher-order
   abstract syntax with proper binding and type information already available.
 
   As a rule of thumb, anything that manipulates bindings of variables or
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -26,8 +26,7 @@
   theory, while \<^verbatim>\<open>x + y\<close> without quotes is not.
 
   Printed theory documents usually omit quotes to gain readability (this is a
-  matter of {\LaTeX} macro setup, say via \<^verbatim>\<open>\isabellestyle\<close>, see also @{cite
-  "isabelle-system"}). Experienced users of Isabelle/Isar may easily
+  matter of {\LaTeX} macro setup, say via \<^verbatim>\<open>\isabellestyle\<close>, see also \<^cite>\<open>"isabelle-system"\<close>). Experienced users of Isabelle/Isar may easily
   reconstruct the lost technical information, while mere readers need not care
   about quotes at all.
 \<close>
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
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -626,7 +626,7 @@
   applied with restriction to the first subgoal, then \<open>m\<^sub>2\<close> is applied
   consecutively with restriction to each subgoal that has newly emerged due to
   \<open>m\<^sub>1\<close>. This is analogous to the tactic combinator \<^ML_infix>\<open>THEN_ALL_NEW\<close> in
-  Isabelle/ML, see also @{cite "isabelle-implementation"}. For example, \<open>(rule
+  Isabelle/ML, see also \<^cite>\<open>"isabelle-implementation"\<close>. For example, \<open>(rule
   r; blast)\<close> applies rule \<open>r\<close> and then solves all new subgoals by \<open>blast\<close>.
 
   Moreover, the explicit goal restriction operator ``\<open>[n]\<close>'' exposes only the
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Isar_Ref/Proof_Script.thy
--- a/src/Doc/Isar_Ref/Proof_Script.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/Proof_Script.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -236,11 +236,10 @@
   \<close>
 
   \<^descr> @{method rule_tac} etc. do resolution of rules with explicit
-  instantiation. This works the same way as the ML tactics \<^ML>\<open>Rule_Insts.res_inst_tac\<close> etc.\ (see @{cite "isabelle-implementation"}).
+  instantiation. This works the same way as the ML tactics \<^ML>\<open>Rule_Insts.res_inst_tac\<close> etc.\ (see \<^cite>\<open>"isabelle-implementation"\<close>).
 
   Multiple rules may be only given if there is no instantiation; then @{method
-  rule_tac} is the same as \<^ML>\<open>resolve_tac\<close> in ML (see @{cite
-  "isabelle-implementation"}).
+  rule_tac} is the same as \<^ML>\<open>resolve_tac\<close> in ML (see \<^cite>\<open>"isabelle-implementation"\<close>).
 
   \<^descr> @{method cut_tac} inserts facts into the proof state as assumption of a
   subgoal; instantiations may be given as well. Note that the scope of
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -456,7 +456,7 @@
   this process, which is called \<^emph>\<open>roundup\<close>, redundant locale instances are
   omitted. A locale instance is redundant if it is subsumed by an instance
   encountered earlier. A more detailed description of this process is
-  available elsewhere @{cite Ballarin2014}.
+  available elsewhere \<^cite>\<open>Ballarin2014\<close>.
 \<close>
 
 
@@ -835,10 +835,10 @@
 
   A class is a particular locale with \<^emph>\<open>exactly one\<close> type variable \<open>\<alpha>\<close>. Beyond
   the underlying locale, a corresponding type class is established which is
-  interpreted logically as axiomatic type class @{cite "Wenzel:1997:TPHOL"}
+  interpreted logically as axiomatic type class \<^cite>\<open>"Wenzel:1997:TPHOL"\<close>
   whose logical content are the assumptions of the locale. Thus, classes
   provide the full generality of locales combined with the commodity of type
-  classes (notably type-inference). See @{cite "isabelle-classes"} for a short
+  classes (notably type-inference). See \<^cite>\<open>"isabelle-classes"\<close> for a short
   tutorial.
 
   \<^rail>\<open>
@@ -983,7 +983,7 @@
   \<^medskip>
   Co-regularity is a very fundamental property of the order-sorted algebra of
   types. For example, it entails principal types and most general unifiers,
-  e.g.\ see @{cite "nipkow-prehofer"}.
+  e.g.\ see \<^cite>\<open>"nipkow-prehofer"\<close>.
 \<close>
 
 
@@ -1009,7 +1009,7 @@
   global constraints on all occurrences. E.g.\ \<open>d :: \<alpha> \<times> \<alpha>\<close> on the left-hand
   side means that all corresponding occurrences on some right-hand side need
   to be an instance of this, and general \<open>d :: \<alpha> \<times> \<beta>\<close> will be disallowed. Full
-  details are given by Kun\v{c}ar @{cite "Kuncar:2015"}.
+  details are given by Kun\v{c}ar \<^cite>\<open>"Kuncar:2015"\<close>.
 
   \<^medskip>
   The \<^theory_text>\<open>consts\<close> command and the \<^theory_text>\<open>overloading\<close> target provide a convenient
@@ -1139,7 +1139,7 @@
   exported to the global bootstrap environment of the ML process --- it has
   a lasting effect that cannot be retracted. This allows ML evaluation
   without a formal theory context, e.g. for command-line tools via @{tool
-  process} @{cite "isabelle-system"}.
+  process} \<^cite>\<open>"isabelle-system"\<close>.
 
   \<^descr> \<^theory_text>\<open>ML_prf\<close> is analogous to \<^theory_text>\<open>ML\<close> but works within a proof context.
   Top-level ML bindings are stored within the proof context in a purely
@@ -1199,14 +1199,14 @@
   debugging information. The global system option @{system_option_ref
   ML_debugger} does the same when building a session image. It is also
   possible use commands like \<^theory_text>\<open>ML_file_debug\<close> etc. The ML debugger is
-  explained further in @{cite "isabelle-jedit"}.
+  explained further in \<^cite>\<open>"isabelle-jedit"\<close>.
 
   \<^descr> @{attribute ML_exception_trace} indicates whether the ML run-time system
   should print a detailed stack trace on exceptions. The result is dependent
   on various ML compiler optimizations. The boundary for the exception trace
   is the current Isar command transactions: it is occasionally better to
   insert the combinator \<^ML>\<open>Runtime.exn_trace\<close> into ML code for debugging
-  @{cite "isabelle-implementation"}, closer to the point where it actually
+  \<^cite>\<open>"isabelle-implementation"\<close>, closer to the point where it actually
   happens.
 
   \<^descr> @{attribute ML_exception_debugger} controls detailed exception trace via
@@ -1258,7 +1258,7 @@
 
     \<^descr>[Exported files] are stored within the session database in
     Isabelle/Scala. This allows to deliver artefacts to external tools, see
-    also @{cite "isabelle-system"} for session \<^verbatim>\<open>ROOT\<close> declaration
+    also \<^cite>\<open>"isabelle-system"\<close> for session \<^verbatim>\<open>ROOT\<close> declaration
     \<^theory_text>\<open>export_files\<close>, and @{tool build} option \<^verbatim>\<open>-e\<close>.
 
   A notable example is the command @{command_ref export_code}
@@ -1323,7 +1323,7 @@
   \<^descr> \<^theory_text>\<open>scala_build_generated_files paths (in thy)\<close> retrieves named generated
   files as for \<^theory_text>\<open>export_generated_files\<close> and writes them into a temporary
   directory, which is taken as starting point for build process of
-  Isabelle/Scala/Java modules (see @{cite "isabelle-system"}). The
+  Isabelle/Scala/Java modules (see \<^cite>\<open>"isabelle-system"\<close>). The
   corresponding @{path \<open>build.props\<close>} file is expected directly in the toplevel
   directory, instead of @{path \<open>etc/build.props\<close>} for Isabelle system
   components. These properties need to specify sources, resources, services
@@ -1356,8 +1356,7 @@
   exports of \<^theory_text>\<open>export_files\<close> above.
 
   \<^descr> \<^theory_text>\<open>external_file name\<close> declares the formal dependency on the given file
-  name, such that the Isabelle build process knows about it (see also @{cite
-  "isabelle-system"}). This is required for any files mentioned in
+  name, such that the Isabelle build process knows about it (see also \<^cite>\<open>"isabelle-system"\<close>). This is required for any files mentioned in
   \<^theory_text>\<open>compile_generated_files / external_files\<close> above, in order to document
   source dependencies properly. It is also possible to use \<^theory_text>\<open>external_file\<close>
   alone, e.g.\ when other Isabelle/ML tools use \<^ML>\<open>File.read\<close>, without
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -10,16 +10,16 @@
 
 text \<open>
   Isabelle/jEdit is a Prover IDE that integrates \<^emph>\<open>parallel proof checking\<close>
-  @{cite "Wenzel:2009" and "Wenzel:2013:ITP"} with \<^emph>\<open>asynchronous user
-  interaction\<close> @{cite "Wenzel:2010" and "Wenzel:2012:UITP-EPTCS" and
-  "Wenzel:2014:ITP-PIDE" and "Wenzel:2014:UITP"}, based on a document-oriented
-  approach to \<^emph>\<open>continuous proof processing\<close> @{cite "Wenzel:2011:CICM" and
-  "Wenzel:2012" and "Wenzel:2018:FIDE" and "Wenzel:2019:MKM"}. Many concepts
+  \<^cite>\<open>"Wenzel:2009" and "Wenzel:2013:ITP"\<close> with \<^emph>\<open>asynchronous user
+  interaction\<close> \<^cite>\<open>"Wenzel:2010" and "Wenzel:2012:UITP-EPTCS" and
+  "Wenzel:2014:ITP-PIDE" and "Wenzel:2014:UITP"\<close>, based on a document-oriented
+  approach to \<^emph>\<open>continuous proof processing\<close> \<^cite>\<open>"Wenzel:2011:CICM" and
+  "Wenzel:2012" and "Wenzel:2018:FIDE" and "Wenzel:2019:MKM"\<close>. Many concepts
   and system components are fit together in order to make this work. The main
   building blocks are as follows.
 
     \<^descr>[Isabelle/ML] is the implementation and extension language of Isabelle,
-    see also @{cite "isabelle-implementation"}. It is integrated into the
+    see also \<^cite>\<open>"isabelle-implementation"\<close>. It is integrated into the
     logical context of Isabelle/Isar and allows to manipulate logical entities
     directly. Arbitrary add-on tools may be implemented for object-logics such
     as Isabelle/HOL.
@@ -84,7 +84,7 @@
   The options allow to specify a logic session name, but the same selector is
   also accessible in the \<^emph>\<open>Theories\<close> panel (\secref{sec:theories}). After
   startup of the Isabelle plugin, the selected logic session image is provided
-  automatically by the Isabelle build tool @{cite "isabelle-system"}: if it is
+  automatically by the Isabelle build tool \<^cite>\<open>"isabelle-system"\<close>: if it is
   absent or outdated wrt.\ its sources, the build process updates it within
   the running text editor. Prover IDE functionality is fully activated after
   successful termination of the build process. A failure may require changing
@@ -171,7 +171,7 @@
 
   Isabelle system options are managed by Isabelle/Scala and changes are stored
   in \<^path>\<open>$ISABELLE_HOME_USER/etc/preferences\<close>, independently of
-  other jEdit properties. See also @{cite "isabelle-system"}, especially the
+  other jEdit properties. See also \<^cite>\<open>"isabelle-system"\<close>, especially the
   coverage of sessions and command-line tools like @{tool build} or @{tool
   options}.
 
@@ -182,8 +182,7 @@
   Isabelle\<close> in jEdit provides a view on a subset of Isabelle system options.
   Note that some of these options affect general parameters that are relevant
   outside Isabelle/jEdit as well, e.g.\ @{system_option threads} or
-  @{system_option parallel_proofs} for the Isabelle build tool @{cite
-  "isabelle-system"}, but it is possible to use the settings variable
+  @{system_option parallel_proofs} for the Isabelle build tool \<^cite>\<open>"isabelle-system"\<close>, but it is possible to use the settings variable
   @{setting ISABELLE_BUILD_OPTIONS} to change defaults for batch builds
   without affecting the Prover IDE.
 
@@ -253,8 +252,7 @@
 
   The \<^verbatim>\<open>-l\<close> option specifies the session name of the logic image to be used
   for proof processing. Additional session root directories may be included
-  via option \<^verbatim>\<open>-d\<close> to augment the session name space (see also @{cite
-  "isabelle-system"}). By default, the specified image is checked and built on
+  via option \<^verbatim>\<open>-d\<close> to augment the session name space (see also \<^cite>\<open>"isabelle-system"\<close>). By default, the specified image is checked and built on
   demand, but option \<^verbatim>\<open>-n\<close> bypasses the implicit build process for the
   selected session image. Options \<^verbatim>\<open>-s\<close> and \<^verbatim>\<open>-u\<close> override the default system
   option @{system_option system_heaps}: this determines where to store the
@@ -277,7 +275,7 @@
 
   The \<^verbatim>\<open>-J\<close> and \<^verbatim>\<open>-j\<close> options pass additional low-level options to the JVM or
   jEdit, respectively. The defaults are provided by the Isabelle settings
-  environment @{cite "isabelle-system"}, but note that these only work for the
+  environment \<^cite>\<open>"isabelle-system"\<close>, but note that these only work for the
   command-line tool described here, and not the desktop application.
 
   The \<^verbatim>\<open>-D\<close> option allows to define JVM system properties; this is passed
@@ -454,7 +452,7 @@
   standards.\<^footnote>\<open>Raw Unicode characters within formal sources compromise
   portability and reliability in the face of changing interpretation of
   special features of Unicode, such as Combining Characters or Bi-directional
-  Text.\<close> See @{cite "Wenzel:2011:CICM"}.
+  Text.\<close> See \<^cite>\<open>"Wenzel:2011:CICM"\<close>.
 
   For the prover back-end, formal text consists of ASCII characters that are
   grouped according to some simple rules, e.g.\ as plain ``\<^verbatim>\<open>a\<close>'' or symbolic
@@ -464,7 +462,7 @@
   in \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and may be augmented by the user in
   \<^path>\<open>$ISABELLE_HOME_USER/etc/symbols\<close>.
 
-  The appendix of @{cite "isabelle-isar-ref"} gives an overview of the
+  The appendix of \<^cite>\<open>"isabelle-isar-ref"\<close> gives an overview of the
   standard interpretation of finitely many symbols from the infinite
   collection. Uninterpreted symbols are displayed literally, e.g.\
   ``\<^verbatim>\<open>\<foobar>\<close>''. Overlap of Unicode characters used in symbol
@@ -718,7 +716,7 @@
     according to a snapshot of the document model. The file browser is \<^emph>\<open>not\<close>
     updated continuously when the PIDE document changes: the reload operation
     needs to be used explicitly. A notable example for exports is the command
-    @{command_ref export_code} @{cite "isabelle-isar-ref"}.
+    @{command_ref export_code} \<^cite>\<open>"isabelle-isar-ref"\<close>.
 
     \<^item> URL \<^verbatim>\<open>isabelle-session:\<close> or action @{action_def
     "isabelle-session-browser"} show the structure of session chapters and
@@ -789,7 +787,7 @@
 
   \<^medskip>
   Isabelle/ML files are structured according to semi-formal comments that are
-  explained in @{cite "isabelle-implementation"}. This outline is turned into
+  explained in \<^cite>\<open>"isabelle-implementation"\<close>. This outline is turned into
   a tree-view by default, by using the \<^verbatim>\<open>isabelle-ml\<close> parser. There is also a
   folding mode of the same name, for hierarchic text folds within ML files.
 
@@ -844,12 +842,11 @@
   nodes in two dimensions:
 
     \<^enum> via \<^bold>\<open>theory imports\<close> that are specified in the \<^emph>\<open>theory header\<close> using
-    concrete syntax of the @{command_ref theory} command @{cite
-    "isabelle-isar-ref"};
+    concrete syntax of the @{command_ref theory} command \<^cite>\<open>"isabelle-isar-ref"\<close>;
 
     \<^enum> via \<^bold>\<open>auxiliary files\<close> that are included into a theory by \<^emph>\<open>load
     commands\<close>, notably @{command_ref ML_file} and @{command_ref SML_file}
-    @{cite "isabelle-isar-ref"}.
+    \<^cite>\<open>"isabelle-isar-ref"\<close>.
 
   In any case, source files are managed by the PIDE infrastructure: the
   physical file-system only plays a subordinate role. The relevant version of
@@ -924,7 +921,7 @@
 
 text \<open>
   Special load commands like @{command_ref ML_file} and @{command_ref
-  SML_file} @{cite "isabelle-isar-ref"} refer to auxiliary files within some
+  SML_file} \<^cite>\<open>"isabelle-isar-ref"\<close> refer to auxiliary files within some
   theory. Conceptually, the file argument of the command extends the theory
   source by the content of the file, but its editor buffer may be loaded~/
   changed~/ saved separately. The PIDE document model propagates changes of
@@ -1182,8 +1179,7 @@
       'solves' | 'simp' ':' @{syntax term} | @{syntax term})
   \<close>
 
-  See also the Isar command @{command_ref find_theorems} in @{cite
-  "isabelle-isar-ref"}.
+  See also the Isar command @{command_ref find_theorems} in \<^cite>\<open>"isabelle-isar-ref"\<close>.
 \<close>
 
 
@@ -1199,8 +1195,7 @@
       ('name' ':' @{syntax name} | 'strict' ':' @{syntax type} | @{syntax type})
   \<close>
 
-  See also the Isar command @{command_ref find_consts} in @{cite
-  "isabelle-isar-ref"}.
+  See also the Isar command @{command_ref find_consts} in \<^cite>\<open>"isabelle-isar-ref"\<close>.
 \<close>
 
 
@@ -1210,8 +1205,7 @@
   The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Print Context\<close> mode prints information from the
   theory or proof context, or proof state. See also the Isar commands
   @{command_ref print_context}, @{command_ref print_cases}, @{command_ref
-  print_term_bindings}, @{command_ref print_theorems}, described in @{cite
-  "isabelle-isar-ref"}.
+  print_term_bindings}, @{command_ref print_theorems}, described in \<^cite>\<open>"isabelle-isar-ref"\<close>.
 \<close>
 
 
@@ -1437,7 +1431,7 @@
 
 text \<open>
   The theory header syntax supports abbreviations via the \<^theory_text>\<open>abbrevs\<close> keyword
-  @{cite "isabelle-isar-ref"}. This is a slight generalization of built-in
+  \<^cite>\<open>"isabelle-isar-ref"\<close>. This is a slight generalization of built-in
   templates and abbreviations for Isabelle symbols, as explained above.
   Examples may be found in the Isabelle sources, by searching for
   ``\<^verbatim>\<open>abbrevs\<close>'' in \<^verbatim>\<open>*.thy\<close> files.
@@ -1757,8 +1751,7 @@
 
   \<^item> @{system_option_ref auto_methods} controls automatic use of a combination
   of standard proof methods (@{method auto}, @{method simp}, @{method blast},
-  etc.). This corresponds to the Isar command @{command_ref "try0"} @{cite
-  "isabelle-isar-ref"}.
+  etc.). This corresponds to the Isar command @{command_ref "try0"} \<^cite>\<open>"isabelle-isar-ref"\<close>.
 
   The tool is disabled by default, since unparameterized invocation of
   standard proof methods often consumes substantial CPU resources without
@@ -1766,7 +1759,7 @@
 
   \<^item> @{system_option_ref auto_nitpick} controls a slightly reduced version of
   @{command_ref nitpick}, which tests for counterexamples using first-order
-  relational logic. See also the Nitpick manual @{cite "isabelle-nitpick"}.
+  relational logic. See also the Nitpick manual \<^cite>\<open>"isabelle-nitpick"\<close>.
 
   This tool is disabled by default, due to the extra overhead of invoking an
   external Java process for each attempt to disprove a subgoal.
@@ -1780,8 +1773,7 @@
 
   \<^item> @{system_option_ref auto_sledgehammer} controls a significantly reduced
   version of @{command_ref sledgehammer}, which attempts to prove a subgoal
-  using external automatic provers. See also the Sledgehammer manual @{cite
-  "isabelle-sledgehammer"}.
+  using external automatic provers. See also the Sledgehammer manual \<^cite>\<open>"isabelle-sledgehammer"\<close>.
 
   This tool is disabled by default, due to the relatively heavy nature of
   Sledgehammer.
@@ -1853,7 +1845,7 @@
 text \<open>
   The ultimate purpose of Isabelle is to produce nicely rendered documents
   with the Isabelle document preparation system, which is based on {\LaTeX};
-  see also @{cite "isabelle-system" and "isabelle-isar-ref"}. Isabelle/jEdit
+  see also \<^cite>\<open>"isabelle-system" and "isabelle-isar-ref"\<close>. Isabelle/jEdit
   provides some additional support for document editing.
 \<close>
 
@@ -1912,12 +1904,10 @@
 
 text \<open>
   Citations are managed by {\LaTeX} and Bib{\TeX} in \<^verbatim>\<open>.bib\<close> files. The
-  Isabelle session build process and the @{tool document} tool @{cite
-  "isabelle-system"} are smart enough to assemble the result, based on the
+  Isabelle session build process and the @{tool document} tool \<^cite>\<open>"isabelle-system"\<close> are smart enough to assemble the result, based on the
   session directory layout.
 
-  The document antiquotation \<open>@{cite}\<close> is described in @{cite
-  "isabelle-isar-ref"}. Within the Prover IDE it provides semantic markup for
+  The document antiquotation \<open>@{cite}\<close> is described in \<^cite>\<open>"isabelle-isar-ref"\<close>. Within the Prover IDE it provides semantic markup for
   tooltips, hyperlinks, and completion for Bib{\TeX} database entries.
   Isabelle/jEdit does \<^emph>\<open>not\<close> know about the actual Bib{\TeX} environment used
   in {\LaTeX} batch-mode, but it can take citations from those \<^verbatim>\<open>.bib\<close> files
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Locales/Examples.thy
--- a/src/Doc/Locales/Examples.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Locales/Examples.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -292,7 +292,7 @@
   exception of the context elements \isakeyword{constrains} and
   \isakeyword{defines}, which are provided for backward
   compatibility.  See the Isabelle/Isar Reference
-  Manual @{cite IsarRef} for full documentation.\<close>
+  Manual \<^cite>\<open>IsarRef\<close> for full documentation.\<close>
 
 
 section \<open>Import \label{sec:import}\<close>
@@ -757,7 +757,7 @@
   The sublocale relation is transitive --- that is, propagation takes
   effect along chains of sublocales.  Even cycles in the sublocale relation are
   supported, as long as these cycles do not lead to infinite chains.
-  Details are discussed in the technical report @{cite Ballarin2006a}.
+  Details are discussed in the technical report \<^cite>\<open>Ballarin2006a\<close>.
   See also Section~\ref{sec:infinite-chains} of this tutorial.\<close>
 
 end
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
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Logics_ZF/ZF_Isar.thy
--- a/src/Doc/Logics_ZF/ZF_Isar.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Logics_ZF/ZF_Isar.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -93,7 +93,7 @@
     hints: @{syntax (ZF) "monos"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
   \<close>
 
-  See @{cite "isabelle-ZF"} for further information on inductive
+  See \<^cite>\<open>"isabelle-ZF"\<close> for further information on inductive
   definitions in ZF, but note that this covers the old-style theory
   format.
 \<close>
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Prog_Prove/Isar.thy
--- a/src/Doc/Prog_Prove/Isar.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Prog_Prove/Isar.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -504,7 +504,7 @@
 Therefore the \isacom{also} hidden in \isacom{finally} sets \<open>calculation\<close>
 to \<open>t\<^sub>1 < t\<^sub>4\<close> and the final ``\texttt{.}'' succeeds.
 
-For more information on this style of proof see @{cite "BauerW-TPHOLs01"}.
+For more information on this style of proof see \<^cite>\<open>"BauerW-TPHOLs01"\<close>.
 \fi
 
 \section{Streamlining Proofs}
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Prog_Prove/Logic.thy
--- a/src/Doc/Prog_Prove/Logic.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Prog_Prove/Logic.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -141,7 +141,7 @@
 @{thm image_def}\index{$IMP042@\<^term>\<open>f ` A\<close>} & is the image of a function over a set
 \end{tabular}
 \end{center}
-See @{cite "Nipkow-Main"} for the wealth of further predefined functions in theory
+See \<^cite>\<open>"Nipkow-Main"\<close> for the wealth of further predefined functions in theory
 \<^theory>\<open>Main\<close>.
 
 
@@ -399,7 +399,7 @@
   {\mbox{\<open>?P = ?Q\<close>}}
 \]
 These rules are part of the logical system of \concept{natural deduction}
-(e.g., @{cite HuthRyan}). Although we intentionally de-emphasize the basic rules
+(e.g., \<^cite>\<open>HuthRyan\<close>). Although we intentionally de-emphasize the basic rules
 of logic in favour of automatic proof methods that allow you to take bigger
 steps, these rules are helpful in locating where and why automation fails.
 When applied backwards, these rules decompose the goal:
@@ -483,7 +483,7 @@
 %
 %Command \isacom{find{\isacharunderscorekeyword}theorems} searches for specific theorems in the current
 %theory. Search criteria include pattern matching on terms and on names.
-%For details see the Isabelle/Isar Reference Manual~@{cite IsarRef}.
+%For details see the Isabelle/Isar Reference Manual~\<^cite>\<open>IsarRef\<close>.
 %\bigskip
 
 \begin{warn}
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Prog_Prove/Types_and_funs.thy
--- a/src/Doc/Prog_Prove/Types_and_funs.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -147,7 +147,7 @@
 fixed argument position decreases in size with each recursive call. The size
 is measured as the number of constructors (excluding 0-ary ones, e.g., \<open>Nil\<close>). Lexicographic combinations are also recognized. In more complicated
 situations, the user may have to prove termination by hand. For details
-see~@{cite Krauss}.
+see~\<^cite>\<open>Krauss\<close>.
 
 Functions defined with \isacom{fun} come with their own induction schema
 that mirrors the recursion schema and is derived from the termination
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Sugar/Sugar.thy
--- a/src/Doc/Sugar/Sugar.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Sugar/Sugar.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -18,7 +18,7 @@
 @{thm[display,mode=latex_sum] sum_Suc_diff[no_vars]}
 No typos, no omissions, no sweat.
 If you have not experienced that joy, read Chapter 4, \emph{Presenting
-Theories}, @{cite LNCS2283} first.
+Theories}, \<^cite>\<open>LNCS2283\<close> first.
 
 If you have mastered the art of Isabelle's \emph{antiquotations},
 i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity
@@ -234,7 +234,7 @@
 \subsection{Inference rules}
 
 To print theorems as inference rules you need to include Didier
-R\'emy's \texttt{mathpartir} package~@{cite mathpartir}
+R\'emy's \texttt{mathpartir} package~\<^cite>\<open>mathpartir\<close>
 for typesetting inference rules in your \LaTeX\ file.
 
 Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/System/Environment.thy
--- a/src/Doc/System/Environment.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/System/Environment.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -8,10 +8,8 @@
 
 text \<open>
   This manual describes Isabelle together with related tools as seen from a
-  system oriented view. See also the \<^emph>\<open>Isabelle/Isar Reference Manual\<close> @{cite
-  "isabelle-isar-ref"} for the actual Isabelle input language and related
-  concepts, and \<^emph>\<open>The Isabelle/Isar Implementation Manual\<close> @{cite
-  "isabelle-implementation"} for the main concepts of the underlying
+  system oriented view. See also the \<^emph>\<open>Isabelle/Isar Reference Manual\<close> \<^cite>\<open>"isabelle-isar-ref"\<close> for the actual Isabelle input language and related
+  concepts, and \<^emph>\<open>The Isabelle/Isar Implementation Manual\<close> \<^cite>\<open>"isabelle-implementation"\<close> for the main concepts of the underlying
   implementation in Isabelle/ML.
 \<close>
 
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/System/Scala.thy
--- a/src/Doc/System/Scala.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/System/Scala.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -13,7 +13,7 @@
     \<^item> Isabelle/ML is for \<^emph>\<open>mathematics\<close>, to develop tools within the context
     of symbolic logic, e.g.\ for constructing proofs or defining
     domain-specific formal languages. See the \<^emph>\<open>Isabelle/Isar implementation
-    manual\<close> @{cite "isabelle-implementation"} for more details.
+    manual\<close> \<^cite>\<open>"isabelle-implementation"\<close> for more details.
 
     \<^item> Isabelle/Scala is for \<^emph>\<open>physics\<close>, to connect with the world of systems
     and services, including editors and IDE frameworks.
@@ -27,7 +27,7 @@
     (\secref{sec:scala-functions}) via the PIDE protocol: execution happens
     within the running Java process underlying Isabelle/Scala.
 
-    \<^item> The \<^verbatim>\<open>Console/Scala\<close> plugin of Isabelle/jEdit @{cite "isabelle-jedit"}
+    \<^item> The \<^verbatim>\<open>Console/Scala\<close> plugin of Isabelle/jEdit \<^cite>\<open>"isabelle-jedit"\<close>
     operates on the running Java application, using the Scala
     read-eval-print-loop (REPL).
 
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/System/Server.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -463,8 +463,7 @@
   string, id?: long}\<close> describes a source position within Isabelle text. Only
   the \<open>line\<close> and \<open>file\<close> fields make immediate sense to external programs.
   Detailed \<open>offset\<close> and \<open>end_offset\<close> positions are counted according to
-  Isabelle symbols, see \<^ML_type>\<open>Symbol.symbol\<close> in Isabelle/ML @{cite
-  "isabelle-implementation"}. The position \<open>id\<close> belongs to the representation
+  Isabelle symbols, see \<^ML_type>\<open>Symbol.symbol\<close> in Isabelle/ML \<^cite>\<open>"isabelle-implementation"\<close>. The position \<open>id\<close> belongs to the representation
   of command transactions in the Isabelle/PIDE protocol: it normally does not
   occur in externalized positions.
 
@@ -732,7 +731,7 @@
 text \<open>
   The asynchronous notifications of command \<^verbatim>\<open>session_build\<close> mainly serve as
   progress indicator: the output resembles that of the session build window of
-  Isabelle/jEdit after startup @{cite "isabelle-jedit"}.
+  Isabelle/jEdit after startup \<^cite>\<open>"isabelle-jedit"\<close>.
 
   For the client it is usually sufficient to print the messages in plain text,
   but note that \<open>theory_progress\<close> also reveals formal \<open>theory\<close> and
@@ -1012,7 +1011,7 @@
   \<^item> \<open>theory_name\<close>: the logical theory name;
 
   \<^item> \<open>status\<close>: the overall node status, e.g.\ see the visualization in the
-  \<open>Theories\<close> panel of Isabelle/jEdit @{cite "isabelle-jedit"};
+  \<open>Theories\<close> panel of Isabelle/jEdit \<^cite>\<open>"isabelle-jedit"\<close>;
 
   \<^item> \<open>messages\<close>: the main bulk of prover messages produced in this theory
   (with kind \<^verbatim>\<open>writeln\<close>, \<^verbatim>\<open>warning\<close>, \<^verbatim>\<open>error\<close>).
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/System/Sessions.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -36,7 +36,7 @@
   additional project directories given by the user.
 
   The ROOT file format follows the lexical conventions of the \<^emph>\<open>outer syntax\<close>
-  of Isabelle/Isar, see also @{cite "isabelle-isar-ref"}. This defines common
+  of Isabelle/Isar, see also \<^cite>\<open>"isabelle-isar-ref"\<close>. This defines common
   forms like identifiers, names, quoted strings, verbatim text, nested
   comments etc. The grammar for @{syntax chapter_def}, @{syntax chapter_entry}
   and @{syntax session_entry} is given as syntax diagram below. Each ROOT file
@@ -45,7 +45,7 @@
   chapter is ``\<open>Unsorted\<close>''. Chapter definitions, which are optional, allow to
   associate additional information.
 
-  Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple editing mode
+  Isabelle/jEdit \<^cite>\<open>"isabelle-jedit"\<close> includes a simple editing mode
   \<^verbatim>\<open>isabelle-root\<close> for session ROOT files, which is enabled by default for any
   file of that name.
 
@@ -192,7 +192,7 @@
   tools require global configuration during system startup. An empty list of
   \<open>patterns\<close> defaults to \<^verbatim>\<open>"*:classpath/*.jar"\<close>, which fits to the naming
   convention of JAR modules produced by the Isabelle/Isar command
-  \<^theory_text>\<open>scala_build_generated_files\<close> @{cite "isabelle-isar-ref"}.
+  \<^theory_text>\<open>scala_build_generated_files\<close> \<^cite>\<open>"isabelle-isar-ref"\<close>.
 \<close>
 
 
@@ -211,7 +211,7 @@
 
 text \<open>
   See \<^file>\<open>~~/etc/options\<close> for the main defaults provided by the Isabelle
-  distribution. Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple
+  distribution. Isabelle/jEdit \<^cite>\<open>"isabelle-jedit"\<close> includes a simple
   editing mode \<^verbatim>\<open>isabelle-options\<close> for this file-format.
 
   The following options are particularly relevant to build Isabelle sessions,
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Tutorial/Advanced/simp2.thy
--- a/src/Doc/Tutorial/Advanced/simp2.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/Advanced/simp2.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -122,7 +122,7 @@
 rewrite rules. This is not quite true.  For reasons of feasibility,
 the simplifier expects the
 left-hand side of each rule to be a so-called \emph{higher-order
-pattern}~@{cite "nipkow-patterns"}\indexbold{patterns!higher-order}. 
+pattern}~\<^cite>\<open>"nipkow-patterns"\<close>\indexbold{patterns!higher-order}. 
 This restricts where
 unknowns may occur.  Higher-order patterns are terms in $\beta$-normal
 form.  (This means there are no subterms of the form $(\lambda x. M)(N)$.)  
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Tutorial/CTL/Base.thy
--- a/src/Doc/Tutorial/CTL/Base.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/CTL/Base.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -7,7 +7,7 @@
 Computation Tree Logic (CTL), a temporal logic.
 Model checking is a popular technique for the verification of finite
 state systems (implementations) with respect to temporal logic formulae
-(specifications) @{cite "ClarkeGP-book" and "Huth-Ryan-book"}. Its foundations are set theoretic
+(specifications) \<^cite>\<open>"ClarkeGP-book" and "Huth-Ryan-book"\<close>. Its foundations are set theoretic
 and this section will explore them in HOL\@. This is done in two steps.  First
 we consider a simple modal logic called propositional dynamic
 logic (PDL)\@.  We then proceed to the temporal logic CTL, which is
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Tutorial/CTL/CTL.thy
--- a/src/Doc/Tutorial/CTL/CTL.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/CTL/CTL.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -361,7 +361,7 @@
 %{text[display]"| EU formula formula    E[_ U _]"}
 %which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
 \end{exercise}
-For more CTL exercises see, for example, Huth and Ryan @{cite "Huth-Ryan-book"}.
+For more CTL exercises see, for example, Huth and Ryan \<^cite>\<open>"Huth-Ryan-book"\<close>.
 \<close>
 
 (*<*)
@@ -439,7 +439,7 @@
 our model checkers.  It is clear that if all sets are finite, they can be
 represented as lists and the usual set operations are easily
 implemented. Only \<^const>\<open>lfp\<close> requires a little thought.  Fortunately, theory
-\<open>While_Combinator\<close> in the Library~@{cite "HOL-Library"} provides a
+\<open>While_Combinator\<close> in the Library~\<^cite>\<open>"HOL-Library"\<close> provides a
 theorem stating that in the case of finite sets and a monotone
 function~\<^term>\<open>F\<close>, the value of \mbox{\<^term>\<open>lfp F\<close>} can be computed by
 iterated application of \<^term>\<open>F\<close> to~\<^term>\<open>{}\<close> until a fixed point is
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Tutorial/CTL/PDL.thy
--- a/src/Doc/Tutorial/CTL/PDL.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/CTL/PDL.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -8,7 +8,7 @@
 connectives \<open>AX\<close> and \<open>EF\<close>\@. Since formulae are essentially
 syntax trees, they are naturally modelled as a datatype:%
 \footnote{The customary definition of PDL
-@{cite "HarelKT-DL"} looks quite different from ours, but the two are easily
+\<^cite>\<open>"HarelKT-DL"\<close> looks quite different from ours, but the two are easily
 shown to be equivalent.}
 \<close>
 
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Tutorial/Datatype/Nested.thy
--- a/src/Doc/Tutorial/Datatype/Nested.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/Datatype/Nested.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -149,7 +149,7 @@
 instead.  Simple uses of \isacommand{fun} are described in
 \S\ref{sec:fun} below.  Advanced applications, including functions
 over nested datatypes like \<open>term\<close>, are discussed in a
-separate tutorial~@{cite "isabelle-function"}.
+separate tutorial~\<^cite>\<open>"isabelle-function"\<close>.
 
 Of course, you may also combine mutual and nested recursion of datatypes. For example,
 constructor \<open>Sum\<close> in \S\ref{sec:datatype-mut-rec} could take a list of
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
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Tutorial/Fun/fun0.thy
--- a/src/Doc/Tutorial/Fun/fun0.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/Fun/fun0.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -96,7 +96,7 @@
 
 text\<open>The order of arguments has no influence on whether
 \isacommand{fun} can prove termination of a function. For more details
-see elsewhere~@{cite bulwahnKN07}.
+see elsewhere~\<^cite>\<open>bulwahnKN07\<close>.
 
 \subsection{Simplification}
 \label{sec:fun-simplification}
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Tutorial/Inductive/AB.thy
--- a/src/Doc/Tutorial/Inductive/AB.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/Inductive/AB.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -17,7 +17,7 @@
 B &\to& b S \mid a B B \nonumber
 \end{eqnarray}
 At the end we say a few words about the relationship between
-the original proof @{cite \<open>p.\ts81\<close> HopcroftUllman} and our formal version.
+the original proof \<^cite>\<open>\<open>p.\ts81\<close> in HopcroftUllman\<close> and our formal version.
 
 We start by fixing the alphabet, which consists only of \<^term>\<open>a\<close>'s
 and~\<^term>\<open>b\<close>'s:
@@ -278,7 +278,7 @@
 text\<open>
 We conclude this section with a comparison of our proof with 
 Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.}
-@{cite \<open>p.\ts81\<close> HopcroftUllman}.
+\<^cite>\<open>\<open>p.\ts81\<close> in HopcroftUllman\<close>.
 For a start, the textbook
 grammar, for no good reason, excludes the empty word, thus complicating
 matters just a little bit: they have 8 instead of our 7 productions.
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Tutorial/Protocol/NS_Public.thy
--- a/src/Doc/Tutorial/Protocol/NS_Public.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/Protocol/NS_Public.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -381,8 +381,8 @@
 \medskip
 
 Detailed information on this protocol verification technique can be found
-elsewhere~@{cite "paulson-jcs"}, including proofs of an Internet
-protocol~@{cite "paulson-tls"}.  We must stress that the protocol discussed
+elsewhere~\<^cite>\<open>"paulson-jcs"\<close>, including proofs of an Internet
+protocol~\<^cite>\<open>"paulson-tls"\<close>.  We must stress that the protocol discussed
 in this chapter is trivial.  There are only three messages; no keys are
 exchanged; we merely have to prove that encrypted data remains secret. 
 Real world protocols are much longer and distribute many secrets to their
@@ -391,7 +391,7 @@
 been used to encrypt other sensitive information, there may be cascading
 losses.  We may still be able to establish a bound on the losses and to
 prove that other protocol runs function
-correctly~@{cite "paulson-yahalom"}.  Proofs of real-world protocols follow
+correctly~\<^cite>\<open>"paulson-yahalom"\<close>.  Proofs of real-world protocols follow
 the strategy illustrated above, but the subgoals can
 be much bigger and there are more of them.
 \index{protocols!security|)}
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Tutorial/Types/Axioms.thy
--- a/src/Doc/Tutorial/Types/Axioms.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/Types/Axioms.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -8,7 +8,7 @@
 
 \begin{warn}
 Proofs in this section use structured \emph{Isar} proofs, which are not
-covered in this tutorial; but see @{cite "Nipkow-TYPES02"}.%
+covered in this tutorial; but see \<^cite>\<open>"Nipkow-TYPES02"\<close>.%
 \end{warn}\<close>
 
 subsubsection \<open>Semigroups\<close>
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Tutorial/Types/Records.thy
--- a/src/Doc/Tutorial/Types/Records.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/Types/Records.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -33,7 +33,7 @@
 
 text \<open>
   Record types are not primitive in Isabelle and have a delicate
-  internal representation @{cite "NaraschewskiW-TPHOLs98"}, based on
+  internal representation \<^cite>\<open>"NaraschewskiW-TPHOLs98"\<close>, based on
   nested copies of the primitive product type.  A \commdx{record}
   declaration introduces a new record type scheme by specifying its
   fields, which are packaged internally to hold up the perception of
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Tutorial/Types/Typedefs.thy
--- a/src/Doc/Tutorial/Types/Typedefs.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Tutorial/Types/Typedefs.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -213,7 +213,7 @@
 example to demonstrate \isacommand{typedef} because its simplicity makes the
 key concepts particularly easy to grasp. If you would like to see a
 non-trivial example that cannot be defined more directly, we recommend the
-definition of \emph{finite multisets} in the Library~@{cite "HOL-Library"}.
+definition of \emph{finite multisets} in the Library~\<^cite>\<open>"HOL-Library"\<close>.
 
 Let us conclude by summarizing the above procedure for defining a new type.
 Given some abstract axiomatic description $P$ of a type $ty$ in terms of a
diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy
--- a/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -28,8 +28,8 @@
   instantiating type-classes, adding relationships between
   locales (@{command sublocale}) and type-classes
   (@{command subclass}).  Handy introductions are the
-  respective tutorials @{cite "isabelle-locale"}
-  @{cite "isabelle-classes"}.
+  respective tutorials \<^cite>\<open>"isabelle-locale"\<close>
+  \<^cite>\<open>"isabelle-classes"\<close>.
 \<close>
 
 subsection \<open>Strengths and restrictions of type classes\<close>
@@ -48,7 +48,7 @@
   to the numerical type on the right hand side.
 
   How to accomplish this given the quite restrictive type system
-  of {Isabelle/HOL}?  Paulson @{cite "paulson-numerical"} explains
+  of {Isabelle/HOL}?  Paulson \<^cite>\<open>"paulson-numerical"\<close> explains
   that each numerical type has some characteristic properties
   which define an characteristic algebraic structure;  \<open>\<sqsubset>\<close>
   then corresponds to specialization of the corresponding
@@ -122,7 +122,7 @@
   optionally showing the logical content for each class also.
   Optional parameters restrict the graph to a particular segment
   which is useful to get a graspable view.  See
-  the Isar reference manual @{cite "isabelle-isar-ref"} for details.
+  the Isar reference manual \<^cite>\<open>"isabelle-isar-ref"\<close> for details.
 \<close>
 
 
@@ -144,7 +144,7 @@
     \<^item> @{command class} \<^class>\<open>one\<close> with @{term [source] "1::'a::one"}
 
   \noindent Before the introduction of the @{command class} statement in
-  Isabelle @{cite "Haftmann-Wenzel:2006:classes"} it was impossible
+  Isabelle \<^cite>\<open>"Haftmann-Wenzel:2006:classes"\<close> it was impossible
   to define operations with associated axioms in the same class,
   hence there were always pairs of syntactic and logical type
   classes.  This restriction is lifted nowadays, but there are
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Algebra/Group.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -14,7 +14,7 @@
 subsection \<open>Definitions\<close>
 
 text \<open>
-  Definitions follow @{cite "Jacobson:1985"}.
+  Definitions follow \<^cite>\<open>"Jacobson:1985"\<close>.
 \<close>
 
 record 'a monoid =  "'a partial_object" +
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Algebra/Multiplicative_Group.thy
--- a/src/HOL/Algebra/Multiplicative_Group.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Algebra/Multiplicative_Group.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -904,7 +904,7 @@
 text \<open>
   In this section we show that the multiplicative group of a finite field
   is generated by a single element, i.e. it is cyclic. The proof is inspired
-  by the first proof given in the survey~@{cite "conrad-cyclicity"}.
+  by the first proof given in the survey~\<^cite>\<open>"conrad-cyclicity"\<close>.
 \<close>
 
 context field begin
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Algebra/Sylow.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -6,7 +6,7 @@
   imports Coset Exponent
 begin
 
-text \<open>See also @{cite "Kammueller-Paulson:1999"}.\<close>
+text \<open>See also \<^cite>\<open>"Kammueller-Paulson:1999"\<close>.\<close>
 
 text \<open>The combinatorial argument is in theory \<open>Exponent\<close>.\<close>
 
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -18,7 +18,7 @@
   carrier set is a set of bounded functions from Nat to the
   coefficient domain.  Bounded means that these functions return zero
   above a certain bound (the degree).  There is a chapter on the
-  formalisation of polynomials in the PhD thesis @{cite "Ballarin:1999"},
+  formalisation of polynomials in the PhD thesis \<^cite>\<open>"Ballarin:1999"\<close>,
   which was implemented with axiomatic type classes.  This was later
   ported to Locales.
 \<close>
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Analysis/Continuous_Extension.thy
--- a/src/HOL/Analysis/Continuous_Extension.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Analysis/Continuous_Extension.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -296,7 +296,7 @@
 
 subsection\<open>Dugundji's Extension Theorem and Tietze Variants\<close>
 
-text \<open>See \cite{dugundji}.\<close>
+text \<open>See \<^cite>\<open>"dugundji"\<close>.\<close>
 
 lemma convex_supp_sum:
   assumes "convex S" and 1: "supp_sum u I = 1"
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Analysis/Infinite_Sum.thy
--- a/src/HOL/Analysis/Infinite_Sum.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Analysis/Infinite_Sum.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -17,7 +17,7 @@
 Our definition is quite standard: $s:=\sum_{x\in A} f(x)$ is the limit of finite sums $s_F:=\sum_{x\in F} f(x)$ for increasing $F$.
 That is, $s$ is the limit of the net $s_F$ where $F$ are finite subsets of $A$ ordered by inclusion.
 We believe that this is the standard definition for such sums.
-See, e.g., Definition 4.11 in \cite{conway2013course}.
+See, e.g., Definition 4.11 in \<^cite>\<open>"conway2013course"\<close>.
 This definition is quite general: it is well-defined whenever $f$ takes values in some
 commutative monoid endowed with a Hausdorff topology.
 (Examples are reals, complex numbers, normed vector spaces, and more.)\<close>
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Analysis/Metric_Arith.thy
--- a/src/HOL/Analysis/Metric_Arith.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Analysis/Metric_Arith.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -12,7 +12,7 @@
 
 text\<^marker>\<open>tag unimportant\<close> \<open>
 A port of the decision procedure ``Formalization of metric spaces in HOL Light''
-@{cite "DBLP:journals/jar/Maggesi18"} for the type class @{class metric_space},
+\<^cite>\<open>"DBLP:journals/jar/Maggesi18"\<close> for the type class @{class metric_space},
 with the \<open>Argo\<close> solver as backend.
 \<close>
 
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Data_Structures/Braun_Tree.thy
--- a/src/HOL/Data_Structures/Braun_Tree.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Data_Structures/Braun_Tree.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -6,8 +6,8 @@
 imports "HOL-Library.Tree_Real"
 begin
 
-text \<open>Braun Trees were studied by Braun and Rem~\cite{BraunRem}
-and later Hoogerwoord~\cite{Hoogerwoord}.\<close>
+text \<open>Braun Trees were studied by Braun and Rem~\<^cite>\<open>"BraunRem"\<close>
+and later Hoogerwoord~\<^cite>\<open>"Hoogerwoord"\<close>.\<close>
 
 fun braun :: "'a tree \<Rightarrow> bool" where
 "braun Leaf = True" |
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Examples/Cantor.thy
--- a/src/HOL/Examples/Cantor.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Examples/Cantor.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -81,7 +81,7 @@
 text \<open>
   The following treatment of Cantor's Theorem follows the classic example from
   the early 1990s, e.g.\ see the file \<^verbatim>\<open>92/HOL/ex/set.ML\<close> in
-  Isabelle92 or @{cite \<open>\S18.7\<close> "paulson-isa-book"}. The old tactic scripts
+  Isabelle92 or \<^cite>\<open>\<open>\S18.7\<close> in "paulson-isa-book"\<close>. The old tactic scripts
   synthesize key information of the proof by refinement of schematic goal
   states. In contrast, the Isar proof needs to say explicitly what is proven.
 
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Examples/Knaster_Tarski.thy
--- a/src/HOL/Examples/Knaster_Tarski.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Examples/Knaster_Tarski.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -16,7 +16,7 @@
 subsection \<open>Prose version\<close>
 
 text \<open>
-  According to the textbook @{cite \<open>pages 93--94\<close> "davey-priestley"}, the
+  According to the textbook \<^cite>\<open>\<open>pages 93--94\<close> in "davey-priestley"\<close>, the
   Knaster-Tarski fixpoint theorem is as follows.\<^footnote>\<open>We have dualized the
   argument, and tuned the notation a little bit.\<close>
 
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/HOLCF/IMP/HoareEx.thy
--- a/src/HOL/HOLCF/IMP/HoareEx.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/HOLCF/IMP/HoareEx.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -9,7 +9,7 @@
 
 text \<open>
   An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch
-  @{cite MuellerNvOS99}.  It demonstrates fixpoint reasoning by showing
+  \<^cite>\<open>MuellerNvOS99\<close>.  It demonstrates fixpoint reasoning by showing
   the correctness of the Hoare rule for while-loops.
 \<close>
 
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Hahn_Banach/Hahn_Banach.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -10,7 +10,7 @@
 
 text \<open>
   We present the proof of two different versions of the Hahn-Banach Theorem,
-  closely following @{cite \<open>\S36\<close> "Heuser:1986"}.
+  closely following \<^cite>\<open>\<open>\S36\<close> in "Heuser:1986"\<close>.
 \<close>
 
 
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Imperative_HOL/Overview.thy
--- a/src/HOL/Imperative_HOL/Overview.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Imperative_HOL/Overview.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -20,8 +20,8 @@
 text \<open>
   \<open>Imperative HOL\<close> is a lightweight framework for reasoning
   about imperative data structures in \<open>Isabelle/HOL\<close>
-  @{cite "Nipkow-et-al:2002:tutorial"}.  Its basic ideas are described in
-  @{cite "Bulwahn-et-al:2008:imp_HOL"}.  However their concrete
+  \<^cite>\<open>"Nipkow-et-al:2002:tutorial"\<close>.  Its basic ideas are described in
+  \<^cite>\<open>"Bulwahn-et-al:2008:imp_HOL"\<close>.  However their concrete
   realisation has changed since, due to both extensions and
   refinements.  Therefore this overview wants to present the framework
   \qt{as it is} by now.  It focusses on the user-view, less on matters
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Induct/Comb.thy
--- a/src/HOL/Induct/Comb.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Induct/Comb.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -11,7 +11,7 @@
 
 text \<open>
   Combinator terms do not have free variables.
-  Example taken from @{cite camilleri92}.
+  Example taken from \<^cite>\<open>camilleri92\<close>.
 \<close>
 
 subsection \<open>Definitions\<close>
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Isar_Examples/Basic_Logic.thy
--- a/src/HOL/Isar_Examples/Basic_Logic.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Isar_Examples/Basic_Logic.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -250,8 +250,7 @@
 subsection \<open>A few examples from ``Introduction to Isabelle''\<close>
 
 text \<open>
-  We rephrase some of the basic reasoning examples of @{cite
-  "isabelle-intro"}, using HOL rather than FOL.
+  We rephrase some of the basic reasoning examples of \<^cite>\<open>"isabelle-intro"\<close>, using HOL rather than FOL.
 \<close>
 
 
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Isar_Examples/Fibonacci.thy
--- a/src/HOL/Isar_Examples/Fibonacci.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Isar_Examples/Fibonacci.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -19,7 +19,7 @@
 begin
 
 text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry
-  Paulson. A few proofs of laws taken from @{cite "Concrete-Math"}.\<close>\<close>
+  Paulson. A few proofs of laws taken from \<^cite>\<open>"Concrete-Math"\<close>.\<close>\<close>
 
 subsection \<open>Fibonacci numbers\<close>
 
@@ -42,11 +42,11 @@
 
 subsection \<open>Fib and gcd commute\<close>
 
-text \<open>A few laws taken from @{cite "Concrete-Math"}.\<close>
+text \<open>A few laws taken from \<^cite>\<open>"Concrete-Math"\<close>.\<close>
 
 lemma fib_add: "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n"
   (is "?P n")
-  \<comment> \<open>see @{cite \<open>page 280\<close> "Concrete-Math"}\<close>
+  \<comment> \<open>see \<^cite>\<open>\<open>page 280\<close> in "Concrete-Math"\<close>\<close>
 proof (induct n rule: fib_induct)
   show "?P 0" by simp
   show "?P 1" by simp
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Isar_Examples/Hoare.thy
--- a/src/HOL/Isar_Examples/Hoare.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -15,8 +15,8 @@
 text \<open>
   The following abstract syntax and semantics of Hoare Logic over \<^verbatim>\<open>WHILE\<close>
   programs closely follows the existing tradition in Isabelle/HOL of
-  formalizing the presentation given in @{cite \<open>\S6\<close> "Winskel:1993"}. See also
-  \<^dir>\<open>~~/src/HOL/Hoare\<close> and @{cite "Nipkow:1998:Winskel"}.
+  formalizing the presentation given in \<^cite>\<open>\<open>\S6\<close> in "Winskel:1993"\<close>. See also
+  \<^dir>\<open>~~/src/HOL/Hoare\<close> and \<^cite>\<open>"Nipkow:1998:Winskel"\<close>.
 \<close>
 
 type_synonym 'a bexp = "'a set"
@@ -60,7 +60,7 @@
 
 text \<open>
   From the semantics defined above, we derive the standard set of primitive
-  Hoare rules; e.g.\ see @{cite \<open>\S6\<close> "Winskel:1993"}. Usually, variant forms
+  Hoare rules; e.g.\ see \<^cite>\<open>\<open>\S6\<close> in "Winskel:1993"\<close>. Usually, variant forms
   of these rules are applied in actual proof, see also \S\ref{sec:hoare-isar}
   and \S\ref{sec:hoare-vcg}.
 
@@ -304,8 +304,7 @@
 
 text \<open>
   Note that above formulation of assignment corresponds to our preferred way
-  to model state spaces, using (extensible) record types in HOL @{cite
-  "Naraschewski-Wenzel:1998:HOOL"}. For any record field \<open>x\<close>, Isabelle/HOL
+  to model state spaces, using (extensible) record types in HOL \<^cite>\<open>"Naraschewski-Wenzel:1998:HOOL"\<close>. For any record field \<open>x\<close>, Isabelle/HOL
   provides a functions \<open>x\<close> (selector) and \<open>x_update\<close> (update). Above, there is
   only a place-holder appearing for the latter kind of function: due to
   concrete syntax \<open>\<acute>x := \<acute>a\<close> also contains \<open>x_update\<close>.\<^footnote>\<open>Note that due to the
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Isar_Examples/Mutilated_Checkerboard.thy
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -10,8 +10,7 @@
 begin
 
 text \<open>
-  The Mutilated Checker Board Problem, formalized inductively. See @{cite
-  "paulson-mutilated-board"} for the original tactic script version.
+  The Mutilated Checker Board Problem, formalized inductively. See \<^cite>\<open>"paulson-mutilated-board"\<close> for the original tactic script version.
 \<close>
 
 subsection \<open>Tilings\<close>
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Lattice/CompleteLattice.thy
--- a/src/HOL/Lattice/CompleteLattice.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Lattice/CompleteLattice.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -106,7 +106,7 @@
 text \<open>
   The Knaster-Tarski Theorem (in its simplest formulation) states that
   any monotone function on a complete lattice has a least fixed-point
-  (see @{cite \<open>pages 93--94\<close> "Davey-Priestley:1990"} for example).  This
+  (see \<^cite>\<open>\<open>pages 93--94\<close> in "Davey-Priestley:1990"\<close> for example).  This
   is a consequence of the basic boundary properties of the complete
   lattice operations.
 \<close>
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Library/BigO.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -14,8 +14,7 @@
 text \<open>
   This library is designed to support asymptotic ``big O'' calculations,
   i.e.~reasoning with expressions of the form \<open>f = O(g)\<close> and \<open>f = g + O(h)\<close>.
-  An earlier version of this library is described in detail in @{cite
-  "Avigad-Donnelly"}.
+  An earlier version of this library is described in detail in \<^cite>\<open>"Avigad-Donnelly"\<close>.
 
   The main changes in this version are as follows:
 
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Library/Code_Lazy.thy
--- a/src/HOL/Library/Code_Lazy.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Library/Code_Lazy.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -15,7 +15,7 @@
 begin
 
 text \<open>
-  This theory and the CodeLazy tool described in @{cite "LochbihlerStoop2018"}.
+  This theory and the CodeLazy tool described in \<^cite>\<open>"LochbihlerStoop2018"\<close>.
 
   It hooks into Isabelle's code generator such that the generated code evaluates a user-specified
   set of type constructors lazily, even in target languages with eager evaluation.
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Library/Poly_Mapping.thy
--- a/src/HOL/Library/Poly_Mapping.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Library/Poly_Mapping.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -295,7 +295,7 @@
       to coefficients.  Lets call this the \emph{ultimate interpretation}.
     \item A further more specialised type isomorphic to @{typ "nat \<Rightarrow>\<^sub>0 'a"}
       is apt to direct implementation using code generation
-      \cite{Haftmann-Nipkow:2010:code}.
+      \<^cite>\<open>"Haftmann-Nipkow:2010:code"\<close>.
   \end{enumerate}
   Note that despite the names \emph{mapping} and \emph{lookup} suggest something
   implementation-near, it is best to keep @{typ "'a \<Rightarrow>\<^sub>0 'b"} as an abstract
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Library/Ramsey.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -916,7 +916,7 @@
 
 text \<open>
   An application of Ramsey's theorem to program termination. See
-  @{cite "Podelski-Rybalchenko"}.
+  \<^cite>\<open>"Podelski-Rybalchenko"\<close>.
 \<close>
 
 definition disj_wf :: "('a \<times> 'a) set \<Rightarrow> bool"
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Proofs/Extraction/Euclid.thy
--- a/src/HOL/Proofs/Extraction/Euclid.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Proofs/Extraction/Euclid.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -16,7 +16,7 @@
 
 text \<open>
   A constructive version of the proof of Euclid's theorem by
-  Markus Wenzel and Freek Wiedijk @{cite "Wenzel-Wiedijk-JAR2002"}.
+  Markus Wenzel and Freek Wiedijk \<^cite>\<open>"Wenzel-Wiedijk-JAR2002"\<close>.
 \<close>
 
 lemma factor_greater_one1: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < m"
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Proofs/Extraction/Higman.thy
--- a/src/HOL/Proofs/Extraction/Higman.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Proofs/Extraction/Higman.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -11,7 +11,7 @@
 
 text \<open>
   Formalization by Stefan Berghofer and Monika Seisenberger,
-  based on Coquand and Fridlender @{cite Coquand93}.
+  based on Coquand and Fridlender \<^cite>\<open>Coquand93\<close>.
 \<close>
 
 datatype letter = A | B
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Proofs/Extraction/Pigeonhole.thy
--- a/src/HOL/Proofs/Extraction/Pigeonhole.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -12,7 +12,7 @@
   We formalize two proofs of the pigeonhole principle, which lead
   to extracted programs of quite different complexity. The original
   formalization of these proofs in {\sc Nuprl} is due to
-  Aleksey Nogin @{cite "Nogin-ENTCS-2000"}.
+  Aleksey Nogin \<^cite>\<open>"Nogin-ENTCS-2000"\<close>.
 
   This proof yields a polynomial program.
 \<close>
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Proofs/Extraction/Warshall.thy
--- a/src/HOL/Proofs/Extraction/Warshall.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Proofs/Extraction/Warshall.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -10,7 +10,7 @@
 
 text \<open>
   Derivation of Warshall's algorithm using program extraction,
-  based on Berger, Schwichtenberg and Seisenberger @{cite "Berger-JAR-2001"}.
+  based on Berger, Schwichtenberg and Seisenberger \<^cite>\<open>"Berger-JAR-2001"\<close>.
 \<close>
 
 datatype b = T | F
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Proofs/Lambda/Eta.thy
--- a/src/HOL/Proofs/Lambda/Eta.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Proofs/Lambda/Eta.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -230,7 +230,7 @@
 
 text \<open>
   Based on a paper proof due to Andreas Abel.
-  Unlike the proof by Masako Takahashi @{cite "Takahashi-IandC"}, it does not
+  Unlike the proof by Masako Takahashi \<^cite>\<open>"Takahashi-IandC"\<close>, it does not
   use parallel eta reduction, which only seems to complicate matters unnecessarily.
 \<close>
 
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Proofs/Lambda/Standardization.thy
--- a/src/HOL/Proofs/Lambda/Standardization.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Proofs/Lambda/Standardization.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -10,8 +10,8 @@
 begin
 
 text \<open>
-Based on lecture notes by Ralph Matthes @{cite "Matthes-ESSLLI2000"},
-original proof idea due to Ralph Loader @{cite Loader1998}.
+Based on lecture notes by Ralph Matthes \<^cite>\<open>"Matthes-ESSLLI2000"\<close>,
+original proof idea due to Ralph Loader \<^cite>\<open>Loader1998\<close>.
 \<close>
 
 
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Proofs/Lambda/StrongNorm.thy
--- a/src/HOL/Proofs/Lambda/StrongNorm.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Proofs/Lambda/StrongNorm.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -9,7 +9,7 @@
 
 text \<open>
 Formalization by Stefan Berghofer. Partly based on a paper proof by
-Felix Joachimski and Ralph Matthes @{cite "Matthes-Joachimski-AML"}.
+Felix Joachimski and Ralph Matthes \<^cite>\<open>"Matthes-Joachimski-AML"\<close>.
 \<close>
 
 
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Proofs/Lambda/WeakNorm.thy
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -11,7 +11,7 @@
 
 text \<open>
 Formalization by Stefan Berghofer. Partly based on a paper proof by
-Felix Joachimski and Ralph Matthes @{cite "Matthes-Joachimski-AML"}.
+Felix Joachimski and Ralph Matthes \<^cite>\<open>"Matthes-Joachimski-AML"\<close>.
 \<close>
 
 
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/SPARK/Manual/Example_Verification.thy
--- a/src/HOL/SPARK/Manual/Example_Verification.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/SPARK/Manual/Example_Verification.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -23,7 +23,7 @@
 We will now explain the usage of the \SPARK{} verification environment by proving
 the correctness of an example program. As an example, we use a program for computing
 the \emph{greatest common divisor} of two natural numbers shown in \figref{fig:gcd-prog},
-which has been taken from the book about \SPARK{} by Barnes @{cite \<open>\S 11.6\<close> Barnes}.
+which has been taken from the book about \SPARK{} by Barnes \<^cite>\<open>\<open>\S 11.6\<close> in Barnes\<close>.
 \<close>
 
 section \<open>Importing \SPARK{} VCs into Isabelle\<close>
@@ -228,7 +228,7 @@
 are trivially proved to be non-negative. Since we are working with non-negative
 numbers, we can also just use \SPARK{}'s \textbf{mod} operator instead of
 \textbf{rem}, which spares us an application of theorems \<open>minus_div_mult_eq_mod [symmetric]\<close>
-and \<open>sdiv_pos_pos\<close>. Finally, as noted by Barnes @{cite \<open>\S 11.5\<close> Barnes},
+and \<open>sdiv_pos_pos\<close>. Finally, as noted by Barnes \<^cite>\<open>\<open>\S 11.5\<close> in Barnes\<close>,
 we can simplify matters by placing the \textbf{assert} statement between
 \textbf{while} and \textbf{loop} rather than directly after the \textbf{loop}.
 In the former case, the loop invariant has to be proved only once, whereas in
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/SPARK/Manual/VC_Principles.thy
--- a/src/HOL/SPARK/Manual/VC_Principles.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/SPARK/Manual/VC_Principles.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -76,7 +76,7 @@
 \caption{Control flow graph for procedure \texttt{Proc2}}
 \label{fig:proc2-graph}
 \end{figure}
-As explained by Barnes @{cite \<open>\S 11.5\<close> Barnes}, the \SPARK{} Examiner unfolds the loop
+As explained by Barnes \<^cite>\<open>\<open>\S 11.5\<close> in Barnes\<close>, the \SPARK{} Examiner unfolds the loop
 \begin{lstlisting}
 for I in T range L .. U loop
   --# assert P (I);
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Unix/Unix.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -67,7 +67,7 @@
   simplification as we just do not intend to discuss a model of multiple
   groups and group membership, but pretend that everyone is member of a single
   global group.\<^footnote>\<open>A general HOL model of user group structures and related
-  issues is given in @{cite "Naraschewski:2001"}.\<close>
+  issues is given in \<^cite>\<open>"Naraschewski:2001"\<close>.\<close>
 \<close>
 
 datatype perm =
@@ -104,7 +104,7 @@
 text \<open>
   In order to model the general tree structure of a Unix file-system we use
   the arbitrarily branching datatype \<^typ>\<open>('a, 'b, 'c) env\<close> from the
-  standard library of Isabelle/HOL @{cite "Bauer-et-al:2002:HOL-Library"}.
+  standard library of Isabelle/HOL \<^cite>\<open>"Bauer-et-al:2002:HOL-Library"\<close>.
   This type provides constructors \<^term>\<open>Val\<close> and \<^term>\<open>Env\<close> as follows:
 
   \<^medskip>
@@ -142,15 +142,14 @@
   @{thm [display, indent = 2, eta_contract = false] lookup_eq [no_vars]}
   @{thm [display, indent = 2, eta_contract = false] update_eq [no_vars]}
 
-  Several further properties of these operations are proven in @{cite
-  "Bauer-et-al:2002:HOL-Library"}. These will be routinely used later on
+  Several further properties of these operations are proven in \<^cite>\<open>"Bauer-et-al:2002:HOL-Library"\<close>. These will be routinely used later on
   without further notice.
 
   \<^bigskip>
   Apparently, the elements of type \<^typ>\<open>file\<close> contain an \<^typ>\<open>att\<close>
   component in either case. We now define a few auxiliary operations to
   manipulate this field uniformly, following the conventions for record types
-  in Isabelle/HOL @{cite "Nipkow-et-al:2000:HOL"}.
+  in Isabelle/HOL \<^cite>\<open>"Nipkow-et-al:2000:HOL"\<close>.
 \<close>
 
 definition
@@ -208,8 +207,7 @@
   access was granted according to the permissions recorded within the
   file-system.
 
-  Note that by the rules of Unix file-system security (e.g.\ @{cite
-  "Tanenbaum:1992"}) both the super-user and owner may always access a file
+  Note that by the rules of Unix file-system security (e.g.\ \<^cite>\<open>"Tanenbaum:1992"\<close>) both the super-user and owner may always access a file
   unconditionally (in our simplified model).
 \<close>
 
@@ -264,8 +262,7 @@
 subsection \<open>Unix system calls \label{sec:unix-syscall}\<close>
 
 text \<open>
-  According to established operating system design (cf.\ @{cite
-  "Tanenbaum:1992"}) user space processes may only initiate system operations
+  According to established operating system design (cf.\ \<^cite>\<open>"Tanenbaum:1992"\<close>) user space processes may only initiate system operations
   by a fixed set of \<^emph>\<open>system-calls\<close>. This enables the kernel to enforce
   certain security policies in the first place.\<^footnote>\<open>Incidently, this is the very
   same principle employed by any ``LCF-style'' theorem proving system
@@ -388,7 +385,7 @@
 
   If in doubt, one may consider to compare our definition with the informal
   specifications given the corresponding Unix man pages, or even peek at an
-  actual implementation such as @{cite "Torvalds-et-al:Linux"}. Another common
+  actual implementation such as \<^cite>\<open>"Torvalds-et-al:Linux"\<close>. Another common
   way to gain confidence into the formal model is to run simple simulations
   (see \secref{sec:unix-examples}), and check the results with that of
   experiments performed on a real Unix system.
diff -r 1e31ddcab458 -r 4c275405faae src/HOL/ex/CTL.thy
--- a/src/HOL/ex/CTL.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/ex/CTL.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -9,8 +9,7 @@
 begin
 
 text \<open>
-  We formalize basic concepts of Computational Tree Logic (CTL) @{cite
-  "McMillan-PhDThesis" and "McMillan-LectureNotes"} within the simply-typed
+  We formalize basic concepts of Computational Tree Logic (CTL) \<^cite>\<open>"McMillan-PhDThesis" and "McMillan-LectureNotes"\<close> within the simply-typed
   set theory of HOL.
 
   By using the common technique of ``shallow embedding'', a CTL formula is
@@ -51,7 +50,7 @@
   holds in a state \<open>s\<close>, iff there is a path, starting from \<open>s\<close>, such that for
   all states \<open>s'\<close> on the path, \<open>p\<close> holds in \<open>s'\<close>. It is easy to see that \<open>\<^bold>E\<^bold>F
   p\<close> and \<open>\<^bold>E\<^bold>G p\<close> may be expressed using least and greatest fixed points
-  @{cite "McMillan-PhDThesis"}.
+  \<^cite>\<open>"McMillan-PhDThesis"\<close>.
 \<close>
 
 definition EX  ("\<^bold>E\<^bold>X _" [80] 90)
diff -r 1e31ddcab458 -r 4c275405faae src/Pure/Examples/Higher_Order_Logic.thy
--- a/src/Pure/Examples/Higher_Order_Logic.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Pure/Examples/Higher_Order_Logic.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -10,8 +10,7 @@
 
 text \<open>
   The following theory development illustrates the foundations of Higher-Order
-  Logic. The ``HOL'' logic that is given here resembles @{cite
-  "Gordon:1985:HOL"} and its predecessor @{cite "church40"}, but the order of
+  Logic. The ``HOL'' logic that is given here resembles \<^cite>\<open>"Gordon:1985:HOL"\<close> and its predecessor \<^cite>\<open>"church40"\<close>, but the order of
   axiomatizations and defined connectives has be adapted to modern
   presentations of \<open>\<lambda>\<close>-calculus and Constructive Type Theory. Thus it fits
   nicely to the underlying Natural Deduction framework of Isabelle/Pure and
diff -r 1e31ddcab458 -r 4c275405faae src/ZF/Induct/Acc.thy
--- a/src/ZF/Induct/Acc.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/ZF/Induct/Acc.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -8,7 +8,7 @@
 theory Acc imports ZF begin
 
 text \<open>
-  Inductive definition of \<open>acc(r)\<close>; see @{cite "paulin-tlca"}.
+  Inductive definition of \<open>acc(r)\<close>; see \<^cite>\<open>"paulin-tlca"\<close>.
 \<close>
 
 consts
diff -r 1e31ddcab458 -r 4c275405faae src/ZF/Induct/Comb.thy
--- a/src/ZF/Induct/Comb.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/ZF/Induct/Comb.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -12,7 +12,7 @@
 text \<open>
   Curiously, combinators do not include free variables.
 
-  Example taken from @{cite camilleri92}.
+  Example taken from \<^cite>\<open>camilleri92\<close>.
 \<close>
 
 
diff -r 1e31ddcab458 -r 4c275405faae src/ZF/Induct/ListN.thy
--- a/src/ZF/Induct/ListN.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/ZF/Induct/ListN.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -9,7 +9,7 @@
 
 text \<open>
   Inductive definition of lists of \<open>n\<close> elements; see
-  @{cite "paulin-tlca"}.
+  \<^cite>\<open>"paulin-tlca"\<close>.
 \<close>
 
 consts listn :: "i\<Rightarrow>i"
diff -r 1e31ddcab458 -r 4c275405faae src/ZF/Induct/Primrec.thy
--- a/src/ZF/Induct/Primrec.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/ZF/Induct/Primrec.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -8,9 +8,9 @@
 theory Primrec imports ZF begin
 
 text \<open>
-  Proof adopted from @{cite szasz93}.
+  Proof adopted from \<^cite>\<open>szasz93\<close>.
 
-  See also @{cite \<open>page 250, exercise 11\<close> mendelson}.
+  See also \<^cite>\<open>\<open>page 250, exercise 11\<close> in mendelson\<close>.
 \<close>