1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Feb 24 07:06:39 2010 -0800
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Feb 24 20:37:01 2010 +0100
     1.3 @@ -33,14 +33,14 @@
     1.4    \end{matharray}
     1.5  
     1.6    \begin{rail}
     1.7 -    'typedecl' typespec infix?
     1.8 +    'typedecl' typespec mixfix?
     1.9      ;
    1.10      'typedef' altname? abstype '=' repset
    1.11      ;
    1.12  
    1.13      altname: '(' (name | 'open' | 'open' name) ')'
    1.14      ;
    1.15 -    abstype: typespec infix?
    1.16 +    abstype: typespec mixfix?
    1.17      ;
    1.18      repset: term ('morphisms' name name)?
    1.19      ;
    1.20 @@ -372,7 +372,7 @@
    1.21      'rep\_datatype' ('(' (name +) ')')? (term +)
    1.22      ;
    1.23  
    1.24 -    dtspec: parname? typespec infix? '=' (cons + '|')
    1.25 +    dtspec: parname? typespec mixfix? '=' (cons + '|')
    1.26      ;
    1.27      cons: name ( type * ) mixfix?
    1.28    \end{rail}
    1.29 @@ -906,6 +906,9 @@
    1.30        \item[iterations] sets how many sets of assignments are
    1.31          generated for each particular size.
    1.32  
    1.33 +      \item[no\_assms] specifies whether assumptions in
    1.34 +        structured proofs should be ignored.
    1.35 +
    1.36      \end{description}
    1.37  
    1.38      These option can be given within square brackets.