updating documentation on quickcheck in the Isar reference
authorbulwahn
Fri Oct 29 08:44:43 2010 +0200 (2010-10-29)
changeset 4024559f011c1877a
parent 40244 783c23f6afbf
child 40246 c03fc7d3fa97
updating documentation on quickcheck in the Isar reference
doc-src/IsarRef/Thy/HOL_Specific.thy
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Oct 28 18:36:34 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 29 08:44:43 2010 +0200
     1.3 @@ -950,6 +950,20 @@
     1.4        \item[no\_assms] specifies whether assumptions in
     1.5          structured proofs should be ignored.
     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.