1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Nov 05 19:22:04 2010 +0100
1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Nov 05 19:39:25 2010 +0100
1.3 @@ -982,20 +982,6 @@
1.4 \item[\isa{expect}] can be used to check if the user's
1.5 expectation was met (\isa{no{\isacharunderscore}expectation}, \isa{no{\isacharunderscore}counterexample}, or \isa{counterexample}).
1.6
1.7 - \item[timeout] sets the time limit in seconds.
1.8 -
1.9 - \item[default\_type] sets the type(s) generally used to instantiate
1.10 - type variables.
1.11 -
1.12 - \item[report] if set quickcheck reports how many tests fulfilled
1.13 - the preconditions.
1.14 -
1.15 - \item[quiet] if not set quickcheck informs about the current size
1.16 - for assignment values.
1.17 -
1.18 - \item[expect] can be used to check if the user's expectation was met
1.19 - (no\_expectation, no\_counterexample, or counterexample)
1.20 -
1.21 \end{description}
1.22
1.23 These option can be given within square brackets.