# HG changeset patch
# User wenzelm
# Date 1428334087 -7200
# Node ID f84b93187ab62d57b0ca4a60f6d7a58be4d7ba4c
# Parent  6eccb133d4e6f19937868f55b30a15691d0116a4
tuned;

diff -r 6eccb133d4e6 -r f84b93187ab6 src/HOL/SPARK/Manual/Reference.thy
--- a/src/HOL/SPARK/Manual/Reference.thy	Mon Apr 06 17:20:10 2015 +0200
+++ b/src/HOL/SPARK/Manual/Reference.thy	Mon Apr 06 17:28:07 2015 +0200
@@ -23,7 +23,9 @@
 \label{sec:spark-commands}
 This section describes the syntax and effect of each of the commands provided
 by HOL-\SPARK{}.
-@{rail "@'spark_open' name ('(' name ')')?"}
+@{rail \<open>
+  @'spark_open' name ('(' name ')')?
+\<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}
@@ -36,7 +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 "@'spark_proof_functions' ((name '=' term)+)"}
+@{rail \<open>
+  @'spark_proof_functions' ((name '=' term)+)
+\<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
@@ -44,8 +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 "@'spark_types' ((name '=' type (mapping?))+);
-mapping: '('((name '=' nameref)+',')')'"}
+@{rail \<open>
+  @'spark_types' ((name '=' type (mapping?))+)
+  ;
+  mapping: '('((name '=' nameref)+',')')'
+\<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
@@ -57,18 +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 "@'spark_status' (('(proved)' | '(unproved)')?)"}
+@{rail \<open>
+  @'spark_status' (('(proved)' | '(unproved)')?)
+\<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 "@'spark_vc' name"}
+@{rail \<open>
+  @'spark_vc' name
+\<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 "@'spark_end' '(incomplete)'?"}
+@{rail \<open>
+  @'spark_end' '(incomplete)'?
+\<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