--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Dec 05 12:36:00 2011 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Dec 05 12:36:02 2011 +0100
@@ -1594,6 +1594,10 @@
\item[@{text size}] specifies the maximum size of the search space
for assignment values.
+ \item[@{text genuine_only}] sets quickcheck only to return genuine
+ counterexample, but not potentially spurious counterexamples due
+ to underspecified functions.
+
\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 Mon Dec 05 12:36:00 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Dec 05 12:36:02 2011 +0100
@@ -2348,6 +2348,10 @@
\item[\isa{size}] specifies the maximum size of the search space
for assignment values.
+ \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{eval}] takes a term or a list of terms and evaluates
these terms under the variable assignment found by quickcheck.