diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/SPARK/Manual/Reference.thy
--- a/src/HOL/SPARK/Manual/Reference.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/SPARK/Manual/Reference.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -23,9 +23,9 @@
 \label{sec:spark-commands}
 This section describes the syntax and effect of each of the commands provided
 by HOL-\SPARK{}.
-@{rail \<open>
+\<^rail>\<open>
   @'spark_open' name ('(' name ')')?
-\<close>}
+\<close>
 Opens a new \SPARK{} verification environment and loads a \texttt{*.siv} file with VCs.
 Alternatively, \texttt{*.vcg} files can be loaded using \isa{\isacommand{spark\_open\_vcg}}.
 The corresponding \texttt{*.fdl} and \texttt{*.rls}
@@ -38,9 +38,9 @@
 format \texttt{$p_1$\_\_$\ldots$\_\_$p_n$}. When working with projects consisting of several
 packages, this is necessary in order for the verification environment to be able to map proof
 functions and types defined in Isabelle to their \SPARK{} counterparts.
-@{rail \<open>
+\<^rail>\<open>
   @'spark_proof_functions' ((name '=' term)+)
-\<close>}
+\<close>
 Associates a proof function with the given name to a term. The name should be the full name
 of the proof function as it appears in the \texttt{*.fdl} file, including the package prefix.
 This command can be used both inside and outside a verification environment. The latter
@@ -48,11 +48,11 @@
 or packages, whereas the former allows the given term to refer to the types generated
 by \isa{\isacommand{spark\_open}} for record or enumeration types specified in the
 \texttt{*.fdl} file.
-@{rail \<open>
+\<^rail>\<open>
   @'spark_types' ((name '=' type (mapping?))+)
   ;
   mapping: '('((name '=' name)+',')')'
-\<close>}
+\<close>
 Associates a \SPARK{} type with the given name with an Isabelle type. This command can
 only be used outside a verification environment. The given type must be either a record
 or a datatype, where the names of fields or constructors must either match those of the
@@ -64,24 +64,24 @@
 using Isabelle's commands for defining records or datatypes. Having introduced the
 types, the proof functions can be defined in Isabelle. Finally, both the proof
 functions and the types can be associated with their \SPARK{} counterparts.
-@{rail \<open>
+\<^rail>\<open>
   @'spark_status' (('(proved)' | '(unproved)')?)
-\<close>}
+\<close>
 Outputs the variables declared in the \texttt{*.fdl} file, the rules declared in
 the \texttt{*.rls} file, and all VCs, together with their status (proved, unproved).
 The output can be restricted to the proved or unproved VCs by giving the corresponding
 option to the command.
-@{rail \<open>
+\<^rail>\<open>
   @'spark_vc' name
-\<close>}
+\<close>
 Initiates the proof of the VC with the given name. Similar to the standard
 \isa{\isacommand{lemma}} or \isa{\isacommand{theorem}} commands, this command
 must be followed by a sequence of proof commands. The command introduces the
 hypotheses \texttt{H1} \dots \texttt{H$n$}, as well as the identifiers
 \texttt{?C1} \dots \texttt{?C$m$} corresponding to the conclusions of the VC.
-@{rail \<open>
+\<^rail>\<open>
   @'spark_end' '(incomplete)'?
-\<close>}
+\<close>
 Closes the current verification environment. Unless the \texttt{incomplete}
 option is given, all VCs must have been proved,
 otherwise the command issues an error message. As a side effect, the command
@@ -101,7 +101,7 @@
 subsection \<open>Integers\<close>
 
 text \<open>
-The FDL type \texttt{integer} is modelled by the Isabelle type @{typ int}.
+The FDL type \texttt{integer} is modelled by the Isabelle type \<^typ>\<open>int\<close>.
 While the FDL \texttt{mod} operator behaves in the same way as its Isabelle
 counterpart, this is not the case for the \texttt{div} operator. As has already
 been mentioned in \secref{sec:proving-vcs}, the \texttt{div} operator of \SPARK{}
@@ -146,7 +146,7 @@
 \end{figure}
 The bitwise logical operators of \SPARK{} and FDL are modelled by the operators
 \<open>AND\<close>, \<open>OR\<close> and \<open>XOR\<close> from Isabelle's \<open>Word\<close> library,
-all of which have type @{typ "int \<Rightarrow> int \<Rightarrow> int"}. A list of properties of these
+all of which have type \<^typ>\<open>int \<Rightarrow> int \<Rightarrow> int\<close>. A list of properties of these
 operators that are useful in proofs about \SPARK{} programs are shown in
 \figref{fig:bitwise}
 \<close>
@@ -163,7 +163,7 @@
 \normalsize
 \isacommand{datatype}\ $t$\ =\ $e_1$\ $\mid$\ $e_2$\ $\mid$\ \dots\ $\mid$\ $e_n$
 \end{isabelle}
-The HOL-\SPARK{} environment defines a type class @{class spark_enum} that captures
+The HOL-\SPARK{} environment defines a type class \<^class>\<open>spark_enum\<close> that captures
 the characteristic properties of all enumeration types. It provides the following
 polymorphic functions and constants for all types \<open>'a\<close> of this type class:
 \begin{flushleft}
@@ -174,14 +174,14 @@
 @{term_type [mode=my_constrain] first_el} \\
 @{term_type [mode=my_constrain] last_el}
 \end{flushleft}
-In addition, @{class spark_enum} is a subclass of the @{class linorder} type class,
+In addition, \<^class>\<open>spark_enum\<close> is a subclass of the \<^class>\<open>linorder\<close> type class,
 which allows the comparison operators \<open><\<close> and \<open>\<le>\<close> to be used on
 enumeration types. The polymorphic operations shown above enjoy a number of
 generic properties that hold for all enumeration types. These properties are
 listed in \figref{fig:enum-generic-properties}.
 Moreover, \figref{fig:enum-specific-properties} shows a list of properties
 that are specific to each enumeration type $t$, such as the characteristic
-equations for @{term val} and @{term pos}.
+equations for \<^term>\<open>val\<close> and \<^term>\<open>pos\<close>.
 \begin{figure}[t]
 \begin{center}
 \small