doc-src/IsarRef/Thy/HOL_Specific.thy

       @{text quickcheck_exhaustive_active}, @{text quickcheck_random_active},
       @{text quickcheck_narrowing_active} are set to true.
     \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.
 
     \item[@{text iterations}] sets how many sets of assignments are
     generated for each particular size.

     instantiate type variables.
 
     \item[@{text report}] if set quickcheck reports how many tests
     fulfilled the preconditions.
 
-    \item[@{text quiet}] if not set quickcheck informs about the
-    current size for assignment values.
+    \item[@{text quiet}] if set quickcheck does not output anything
+    while testing.
+    
+    \item[@{text verbose}] if set quickcheck informs about the
+    current size and cardinality while testing.
 
     \item[@{text expect}] can be used to check if the user's
     expectation was met (@{text no_expectation}, @{text
     no_counterexample}, or @{text counterexample}).