equal
deleted
inserted
replaced
91 \begin{matharray}{rcl} |
91 \begin{matharray}{rcl} |
92 \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{attribute} \\ |
92 \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{attribute} \\ |
93 \end{matharray} |
93 \end{matharray} |
94 |
94 |
95 \begin{rail} |
95 \begin{rail} |
96 'split_format' ((( name * ) + 'and') | ('(' 'complete' ')')) |
96 'split_format' '(' 'complete' ')' |
97 ; |
97 ; |
98 \end{rail} |
98 \end{rail} |
99 |
99 |
100 \begin{description} |
100 \begin{description} |
101 |
101 |
102 \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 |
102 \item \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}\ \isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}} causes |
103 canonical form as specified by the arguments given; the \isa{i}-th |
|
104 collection of arguments refers to occurrences in premise \isa{i} |
|
105 of the rule. The ``\isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}}'' option causes \emph{all} |
|
106 arguments in function applications to be represented canonically |
103 arguments in function applications to be represented canonically |
107 according to their tuple type structure. |
104 according to their tuple type structure. |
108 |
105 |
109 Note that these operations tend to invent funny names for new local |
106 Note that this operation tends to invent funny names for new local |
110 parameters to be introduced. |
107 parameters introduced. |
111 |
108 |
112 \end{description}% |
109 \end{description}% |
113 \end{isamarkuptext}% |
110 \end{isamarkuptext}% |
114 \isamarkuptrue% |
111 \isamarkuptrue% |
115 % |
112 % |