--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Dec 05 14:44:46 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Dec 05 14:47:01 2011 +0100
@@ -2346,6 +2346,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.
@@ -2363,8 +2367,11 @@
\item[\isa{report}] if set quickcheck reports how many tests
fulfilled the preconditions.
- \item[\isa{quiet}] if not set quickcheck informs about the
- current size for assignment values.
+ \item[\isa{quiet}] if set quickcheck does not output anything
+ while testing.
+
+ \item[\isa{verbose}] if set quickcheck informs about the
+ current size and cardinality while testing.
\item[\isa{expect}] can be used to check if the user's
expectation was met (\isa{no{\isaliteral{5F}{\isacharunderscore}}expectation}, \isa{no{\isaliteral{5F}{\isacharunderscore}}counterexample}, or \isa{counterexample}).