# HG changeset patch # User bulwahn # Date 1323084988 -3600 # Node ID 46046d8e96590de7d6149893c3a7e97a995b7029 # Parent cb6ddee6a4633931f20c92dc4a80f8c08c4be366 updating documentation about quiet and verbose options in quickcheck diff -r cb6ddee6a463 -r 46046d8e9659 doc-src/IsarRef/Thy/HOL_Specific.thy --- 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 diff -r cb6ddee6a463 -r 46046d8e9659 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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}).