Documented "incomplete" option of spark_end
Fri, 29 Jun 2012 10:08:41 +0200
changeset 48168 e825bbf49363
parent 48167 da1a1eae93fa
child 48169 6404816632f7
Documented "incomplete" option of spark_end
--- a/src/HOL/SPARK/Manual/Reference.thy	Fri Jun 29 09:45:48 2012 +0200
+++ b/src/HOL/SPARK/Manual/Reference.thy	Fri Jun 29 10:08:41 2012 +0200
@@ -67,8 +67,9 @@
 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'"}
-Closes the current verification environment. All VCs must have been proved,
+@{rail "@'spark_end' '(incomplete)'?"}
+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
 generates a proof review (\texttt{*.prv}) file to inform POGS of the proved