diff -r 6fe4abb9437b -r f07b373f25d3 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Mar 23 08:50:40 2011 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Mar 23 08:50:42 2011 +0100
@@ -982,6 +982,9 @@
     \item[@{text size}] specifies the maximum size of the search space
     for assignment values.
 
+    \item[@{text eval}] takes a term or a list of terms and evaluates
+      these terms under the variable assignment found by quickcheck.
+    
     \item[@{text iterations}] sets how many sets of assignments are
     generated for each particular size.