# HG changeset patch
# User wenzelm
# Date 1340811406 -7200
# Node ID ac561771abdbf707809a1bf5b8270fdacde6ebb4
# Parent  0b3fd5ff8ea7b5dbf2841173d59adb2a104fed56# Parent  68a32e12b999fa51e36d9161720450772e9f7473
merged

diff -r 68a32e12b999 -r ac561771abdb doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Jun 27 17:36:24 2012 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Jun 27 17:36:46 2012 +0200
@@ -1888,6 +1888,8 @@
 
     \item[@{text eval}] takes a term or a list of terms and evaluates
     these terms under the variable assignment found by quickcheck.
+    This option is currently only supported by the default
+    (exhaustive) tester.
 
     \item[@{text iterations}] sets how many sets of assignments are
     generated for each particular size.
diff -r 68a32e12b999 -r ac561771abdb doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Jun 27 17:36:24 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Jun 27 17:36:46 2012 +0200
@@ -2671,6 +2671,8 @@
 
     \item[\isa{eval}] takes a term or a list of terms and evaluates
     these terms under the variable assignment found by quickcheck.
+    This option is currently only supported by the default
+    (exhaustive) tester.
 
     \item[\isa{iterations}] sets how many sets of assignments are
     generated for each particular size.