# HG changeset patch
# User bulwahn
# Date 1288941391 -3600
# Node ID 55a1693affb6f29e04a276ede86a6b5568ec13ca
# Parent  82ebdd19c4a44e80e48149cbd0c505c41c734e17
adding documentation of some quickcheck options

diff -r 82ebdd19c4a4 -r 55a1693affb6 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Nov 04 18:01:55 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Nov 05 08:16:31 2010 +0100
@@ -982,6 +982,20 @@
     \item[\isa{expect}] can be used to check if the user's
     expectation was met (\isa{no{\isacharunderscore}expectation}, \isa{no{\isacharunderscore}counterexample}, or \isa{counterexample}).
 
+      \item[timeout] sets the time limit in seconds.
+
+      \item[default\_type] sets the type(s) generally used to instantiate
+        type variables.
+
+      \item[report] if set quickcheck reports how many tests fulfilled
+        the preconditions.
+
+      \item[quiet] if not set quickcheck informs about the current size
+        for assignment values.
+
+      \item[expect] can be used to check if the user's expectation was met
+        (no\_expectation, no\_counterexample, or counterexample)
+
     \end{description}
 
     These option can be given within square brackets.