1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Feb 23 12:14:46 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Feb 23 14:11:36 2010 +0100
     1.3 @@ -893,6 +893,9 @@
     1.4        \item[iterations] sets how many sets of assignments are
     1.5          generated for each particular size.
     1.6  
     1.7 +      \item[no\_assms] specifies whether assumptions in
     1.8 +        structured proofs should be ignored.
     1.9 +
    1.10      \end{description}
    1.11  
    1.12      These option can be given within square brackets.

     2.1 --- a/doc-src/Nitpick/nitpick.tex	Tue Feb 23 12:14:46 2010 +0100
     2.2 +++ b/doc-src/Nitpick/nitpick.tex	Tue Feb 23 14:11:36 2010 +0100
     2.3 @@ -1910,7 +1910,7 @@
     2.4  (\S\ref{output-format}).}
     2.5  
     2.6  \optrue{assms}{no\_assms}
     2.7 -Specifies whether the relevant assumptions in structured proof should be
     2.8 +Specifies whether the relevant assumptions in structured proofs should be
     2.9  considered. The option is implicitly enabled for automatic runs.
    2.10  
    2.11  \nopagebreak