--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Nov 05 23:19:20 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat Nov 06 00:10:32 2010 +0100
@@ -93,21 +93,18 @@
\end{matharray}
\begin{rail}
- 'split_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
+ 'split_format' '(' 'complete' ')'
;
\end{rail}
\begin{description}
- \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
- canonical form as specified by the arguments given; the \isa{i}-th
- collection of arguments refers to occurrences in premise \isa{i}
- of the rule. The ``\isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}}'' option causes \emph{all}
+ \item \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}\ \isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}} causes
arguments in function applications to be represented canonically
according to their tuple type structure.
- Note that these operations tend to invent funny names for new local
- parameters to be introduced.
+ Note that this operation tends to invent funny names for new local
+ parameters introduced.
\end{description}%
\end{isamarkuptext}%