tuned;
authorwenzelm
Mon Apr 06 17:28:07 2015 +0200 (2015-04-06)
changeset 59938f84b93187ab6
parent 59937 6eccb133d4e6
child 59939 7d46aa03696e
tuned;
src/HOL/SPARK/Manual/Reference.thy
     1.1 --- a/src/HOL/SPARK/Manual/Reference.thy	Mon Apr 06 17:20:10 2015 +0200
     1.2 +++ b/src/HOL/SPARK/Manual/Reference.thy	Mon Apr 06 17:28:07 2015 +0200
     1.3 @@ -23,7 +23,9 @@
     1.4  \label{sec:spark-commands}
     1.5  This section describes the syntax and effect of each of the commands provided
     1.6  by HOL-\SPARK{}.
     1.7 -@{rail "@'spark_open' name ('(' name ')')?"}
     1.8 +@{rail \<open>
     1.9 +  @'spark_open' name ('(' name ')')?
    1.10 +\<close>}
    1.11  Opens a new \SPARK{} verification environment and loads a \texttt{*.siv} file with VCs.
    1.12  Alternatively, \texttt{*.vcg} files can be loaded using \isa{\isacommand{spark\_open\_vcg}}.
    1.13  The corresponding \texttt{*.fdl} and \texttt{*.rls}
    1.14 @@ -36,7 +38,9 @@
    1.15  format \texttt{$p_1$\_\_$\ldots$\_\_$p_n$}. When working with projects consisting of several
    1.16  packages, this is necessary in order for the verification environment to be able to map proof
    1.17  functions and types defined in Isabelle to their \SPARK{} counterparts.
    1.18 -@{rail "@'spark_proof_functions' ((name '=' term)+)"}
    1.19 +@{rail \<open>
    1.20 +  @'spark_proof_functions' ((name '=' term)+)
    1.21 +\<close>}
    1.22  Associates a proof function with the given name to a term. The name should be the full name
    1.23  of the proof function as it appears in the \texttt{*.fdl} file, including the package prefix.
    1.24  This command can be used both inside and outside a verification environment. The latter
    1.25 @@ -44,8 +48,11 @@
    1.26  or packages, whereas the former allows the given term to refer to the types generated
    1.27  by \isa{\isacommand{spark\_open}} for record or enumeration types specified in the
    1.28  \texttt{*.fdl} file.
    1.29 -@{rail "@'spark_types' ((name '=' type (mapping?))+);
    1.30 -mapping: '('((name '=' nameref)+',')')'"}
    1.31 +@{rail \<open>
    1.32 +  @'spark_types' ((name '=' type (mapping?))+)
    1.33 +  ;
    1.34 +  mapping: '('((name '=' nameref)+',')')'
    1.35 +\<close>}
    1.36  Associates a \SPARK{} type with the given name with an Isabelle type. This command can
    1.37  only be used outside a verification environment. The given type must be either a record
    1.38  or a datatype, where the names of fields or constructors must either match those of the
    1.39 @@ -57,18 +64,24 @@
    1.40  using Isabelle's commands for defining records or datatypes. Having introduced the
    1.41  types, the proof functions can be defined in Isabelle. Finally, both the proof
    1.42  functions and the types can be associated with their \SPARK{} counterparts.
    1.43 -@{rail "@'spark_status' (('(proved)' | '(unproved)')?)"}
    1.44 +@{rail \<open>
    1.45 +  @'spark_status' (('(proved)' | '(unproved)')?)
    1.46 +\<close>}
    1.47  Outputs the variables declared in the \texttt{*.fdl} file, the rules declared in
    1.48  the \texttt{*.rls} file, and all VCs, together with their status (proved, unproved).
    1.49  The output can be restricted to the proved or unproved VCs by giving the corresponding
    1.50  option to the command.
    1.51 -@{rail "@'spark_vc' name"}
    1.52 +@{rail \<open>
    1.53 +  @'spark_vc' name
    1.54 +\<close>}
    1.55  Initiates the proof of the VC with the given name. Similar to the standard
    1.56  \isa{\isacommand{lemma}} or \isa{\isacommand{theorem}} commands, this command
    1.57  must be followed by a sequence of proof commands. The command introduces the
    1.58  hypotheses \texttt{H1} \dots \texttt{H$n$}, as well as the identifiers
    1.59  \texttt{?C1} \dots \texttt{?C$m$} corresponding to the conclusions of the VC.
    1.60 -@{rail "@'spark_end' '(incomplete)'?"}
    1.61 +@{rail \<open>
    1.62 +  @'spark_end' '(incomplete)'?
    1.63 +\<close>}
    1.64  Closes the current verification environment. Unless the \texttt{incomplete}
    1.65  option is given, all VCs must have been proved,
    1.66  otherwise the command issues an error message. As a side effect, the command