--- 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.
--- 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