# HG changeset patch
# User bulwahn
# Date 1323084962 -3600
# Node ID 6210c350d88bb906fca5aff6f6f299cb5b74e0eb
# Parent  e32dd098f57a6fe1f6162db73b8f99a87ce61e6a
documenting the genuine_only option in quickcheck;

diff -r e32dd098f57a -r 6210c350d88b doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Dec 05 12:36:00 2011 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Dec 05 12:36:02 2011 +0100
@@ -1594,6 +1594,10 @@
     \item[@{text size}] specifies the maximum size of the search space
     for assignment values.
 
+    \item[@{text genuine_only}] sets quickcheck only to return genuine
+      counterexample, but not potentially spurious counterexamples due
+      to underspecified functions.
+    
     \item[@{text eval}] takes a term or a list of terms and evaluates
       these terms under the variable assignment found by quickcheck.
 
diff -r e32dd098f57a -r 6210c350d88b doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Dec 05 12:36:00 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Dec 05 12:36:02 2011 +0100
@@ -2348,6 +2348,10 @@
     \item[\isa{size}] specifies the maximum size of the search space
     for assignment values.
 
+    \item[\isa{genuine{\isaliteral{5F}{\isacharunderscore}}only}] sets quickcheck only to return genuine
+      counterexample, but not potentially spurious counterexamples due
+      to underspecified functions.
+    
     \item[\isa{eval}] takes a term or a list of terms and evaluates
       these terms under the variable assignment found by quickcheck.