updated generated file;
Fri, 03 Dec 2010 17:31:27 +0100
changeset 40937 e2e0ef28d3f8
parent 40936 10aeae27c7a6
child 40938 e258f6817add
updated generated file;
--- 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:
+    \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.