--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Feb 15 23:19:30 2012 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Feb 16 09:18:20 2012 +0100
@@ -1719,6 +1719,12 @@
\item[@{text genuine_only}] sets quickcheck only to return genuine
counterexample, but not potentially spurious counterexamples due
to underspecified functions.
+
+ \item[@{text abort_potential}] sets quickcheck to abort once it
+ found a potentially spurious counterexample and to not continue
+ to search for a further genuine counterexample.
+ For this option to be effective, the @{text genuine_only} option
+ must be set to false.
\item[@{text eval}] takes a term or a list of terms and evaluates
these terms under the variable assignment found by quickcheck.
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Feb 15 23:19:30 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Feb 16 09:18:20 2012 +0100
@@ -2480,6 +2480,12 @@
\item[\isa{genuine{\isaliteral{5F}{\isacharunderscore}}only}] sets quickcheck only to return genuine
counterexample, but not potentially spurious counterexamples due
to underspecified functions.
+
+ \item[\isa{abort{\isaliteral{5F}{\isacharunderscore}}potential}] sets quickcheck to abort once it
+ found a potentially spurious counterexample and to not continue
+ to search for a further genuine counterexample.
+ For this option to be effective, the \isa{genuine{\isaliteral{5F}{\isacharunderscore}}only} option
+ must be set to false.
\item[\isa{eval}] takes a term or a list of terms and evaluates
these terms under the variable assignment found by quickcheck.