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