doc-src/IsarRef/Thy/document/HOL_Specific.tex

       \isa{quickcheck{\isaliteral{5F}{\isacharunderscore}}exhaustive{\isaliteral{5F}{\isacharunderscore}}active}, \isa{quickcheck{\isaliteral{5F}{\isacharunderscore}}random{\isaliteral{5F}{\isacharunderscore}}active},
       \isa{quickcheck{\isaliteral{5F}{\isacharunderscore}}narrowing{\isaliteral{5F}{\isacharunderscore}}active} are set to true.
     \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.
 
     \item[\isa{iterations}] sets how many sets of assignments are
     generated for each particular size.

     instantiate type variables.
 
     \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}).
 
     \end{description}