--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Dec 05 12:36:22 2011 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Dec 05 12:36:28 2011 +0100
@@ -1615,8 +1615,11 @@
\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
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Dec 05 12:36:22 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Dec 05 12:36:28 2011 +0100
@@ -2369,8 +2369,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}).