doc-src/IsarRef/Thy/HOL_Specific.thy
changeset 35331 450ab945c451
parent 34172 4301e9ea1c54
child 35351 7425aece4ee3
     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.