--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Nov 05 19:22:04 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Nov 05 19:39:25 2010 +0100
@@ -982,20 +982,6 @@
\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.