doc-src/IsarRef/Thy/document/HOL_Specific.tex
changeset 40364 55a1693affb6
parent 40255 9ffbc25e1606
child 40380 ae4b67af2f37
     1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu Nov 04 18:01:55 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Nov 05 08:16:31 2010 +0100
     1.3 @@ -982,6 +982,20 @@
     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.