1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Dec 03 17:29:27 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Dec 03 17:31:27 2010 +0100
     1.3 @@ -948,14 +948,21 @@
     1.4      and \emph{code} for code generation in SML.
     1.5  
     1.6    \item \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} tests the current goal for
     1.7 -    counter examples using a series of arbitrary assignments for its
     1.8 +    counter examples using a series of assignments for its
     1.9      free variables; by default the first subgoal is tested, an other
    1.10      can be selected explicitly using an optional goal index.
    1.11 +    Assignments can be chosen exhausting the search space upto a given
    1.12 +    size or using a fixed number of random assignments in the search space.
    1.13 +    By default, quickcheck uses exhaustive testing.
    1.14      A number of configuration options are supported for
    1.15      \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, notably:
    1.16  
    1.17      \begin{description}
    1.18  
    1.19 +    \item[\isa{tester}] specifies how to explore the search space
    1.20 +      (e.g. exhaustive or random).
    1.21 +      An unknown configuration option is treated as an argument to tester,
    1.22 +      making \isa{{\isaliteral{22}{\isachardoublequote}}tester\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} optional.
    1.23      \item[\isa{size}] specifies the maximum size of the search space
    1.24      for assignment values.
    1.25