# HG changeset patch
# User bulwahn
# Date 1288334683 -7200
# Node ID 59f011c1877ab9ff9cdf9e3d5be7de001a661247
# Parent  783c23f6afbfcc98f7d7de00c6f4ce146408b2b9
updating documentation on quickcheck in the Isar reference

diff -r 783c23f6afbf -r 59f011c1877a doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Oct 28 18:36:34 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 29 08:44:43 2010 +0200
@@ -950,6 +950,20 @@
       \item[no\_assms] specifies whether assumptions in
         structured proofs should be ignored.
 
+      \item[timeout] sets the time limit in seconds.
+
+      \item[default\_type] sets the type(s) generally used to instantiate
+        type variables.
+
+      \item[report] if set quickcheck reports how many tests fulfilled
+        the preconditions.
+
+      \item[quiet] if not set quickcheck informs about the current size
+        for assignment values.
+
+      \item[expect] can be used to check if the user's expectation was met
+        (no\_expectation, no\_counterexample, or counterexample)
+
     \end{description}
 
     These option can be given within square brackets.