# 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}).