--- 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.