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.