# HG changeset patch
# User berghofe
# Date 1340957321 -7200
# Node ID e825bbf49363e84df217b4c1709fd472c2c4b768
# Parent  da1a1eae93fa1ba03031e365b762f0a843530c13
Documented "incomplete" option of spark_end

diff -r da1a1eae93fa -r e825bbf49363 src/HOL/SPARK/Manual/Reference.thy
--- 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.