# HG changeset patch
# User bulwahn
# Date 1291362047 -3600
# Node ID 7351c6afb34875c5161c6468472d6093272ea084
# Parent  c288fd2ead5a48d4e61dcd7ae46a3d8c2bab01e1
explaining quickcheck testers in the documentation

diff -r c288fd2ead5a -r 7351c6afb348 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Dec 03 08:40:47 2010 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Dec 03 08:40:47 2010 +0100
@@ -929,14 +929,21 @@
     and \emph{code} for code generation in SML.
 
   \item @{command (HOL) "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
     @{command (HOL) "quickcheck"}, notably:
 
     \begin{description}
 
+    \item[@{text 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 @{text "tester ="} optional.
     \item[@{text size}] specifies the maximum size of the search space
     for assignment values.