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