# HG changeset patch
# User wenzelm
# Date 1291393887 -3600
# Node ID e2e0ef28d3f8754af2d65dd3b3f9532758955369
# Parent  10aeae27c7a603ba8519d1f8aaf95946c8ce3c17
updated generated file;

diff -r 10aeae27c7a6 -r e2e0ef28d3f8 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- 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.