1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Nov 05 23:19:20 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Sat Nov 06 00:10:32 2010 +0100
     1.3 @@ -93,21 +93,18 @@
     1.4    \end{matharray}
     1.5  
     1.6    \begin{rail}
     1.7 -    'split_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
     1.8 +    'split_format' '(' 'complete' ')'
     1.9      ;
    1.10    \end{rail}
    1.11  
    1.12    \begin{description}
    1.13    
    1.14 -  \item \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub m\ {\isasymAND}\ {\isasymdots}\ {\isasymAND}\ q\isactrlsub {\isadigit{1}}\ {\isasymdots}\ q\isactrlsub n{\isachardoublequote}} puts expressions of low-level tuple types into
    1.15 -  canonical form as specified by the arguments given; the \isa{i}-th
    1.16 -  collection of arguments refers to occurrences in premise \isa{i}
    1.17 -  of the rule.  The ``\isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}}'' option causes \emph{all}
    1.18 +  \item \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}\ \isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}} causes
    1.19    arguments in function applications to be represented canonically
    1.20    according to their tuple type structure.
    1.21  
    1.22 -  Note that these operations tend to invent funny names for new local
    1.23 -  parameters to be introduced.
    1.24 +  Note that this operation tends to invent funny names for new local
    1.25 +  parameters introduced.
    1.26  
    1.27    \end{description}%
    1.28  \end{isamarkuptext}%