# HG changeset patch
# User blanchet
# Date 1266930696 -3600
# Node ID 450ab945c4513250555a240513c73a70656525e0
# Parent  956d08ec5d6569df3c30260a4c1f8b18cb92e11e
document Quickcheck's "no_assms" option

diff -r 956d08ec5d65 -r 450ab945c451 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Feb 23 12:14:46 2010 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Feb 23 14:11:36 2010 +0100
@@ -893,6 +893,9 @@
       \item[iterations] sets how many sets of assignments are
         generated for each particular size.
 
+      \item[no\_assms] specifies whether assumptions in
+        structured proofs should be ignored.
+
     \end{description}
 
     These option can be given within square brackets.
diff -r 956d08ec5d65 -r 450ab945c451 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Tue Feb 23 12:14:46 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Tue Feb 23 14:11:36 2010 +0100
@@ -1910,7 +1910,7 @@
 (\S\ref{output-format}).}
 
 \optrue{assms}{no\_assms}
-Specifies whether the relevant assumptions in structured proof should be
+Specifies whether the relevant assumptions in structured proofs should be
 considered. The option is implicitly enabled for automatic runs.
 
 \nopagebreak