--- 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
VCs.