# HG changeset patch # User wenzelm # Date 981154770 -3600 # Node ID 55de839f48505dd574e8d749200f2420a0d31f35 # Parent 932d66879fe797fab6ebe4f59724a3c813fdacd9 'split_format' attribute; diff -r 932d66879fe7 -r 55de839f4850 doc-src/IsarRef/hol.tex --- a/doc-src/IsarRef/hol.tex Fri Feb 02 22:21:06 2001 +0100 +++ b/doc-src/IsarRef/hol.tex Fri Feb 02 23:59:30 2001 +0100 @@ -3,17 +3,24 @@ \section{Miscellaneous attributes}\label{sec:rule-format} -\indexisaratt{rule-format} +\indexisaratt{rule-format}\indexisaratt{split-format} \begin{matharray}{rcl} rule_format & : & \isaratt \\ + split_format & : & \isaratt \\ \end{matharray} \railalias{ruleformat}{rule\_format} \railterm{ruleformat} +\railalias{splitformat}{split\_format} +\railterm{splitformat} +\railterm{complete} + \begin{rail} ruleformat ('(' noasm ')')? ; + splitformat (((name * ) + 'and') | ('(' complete ')')) + ; \end{rail} \begin{descr} @@ -23,6 +30,15 @@ the corresponding meta-logical connectives. By default, the result is fully normalized, including assumptions and conclusions at any depth. The $no_asm$ option restricts the transformation to the conclusion of a rule. + +\item [$split_format~\vec p@1 \dots \vec p@n$] puts tuple objects into + canonical form as specified by the arguments given; $\vec p@i$ refers to + occurrences in premise $i$ of the rule. + + The $split_format~(complete)$ form causes \emph{all} arguments in function + applications to be represented canonically according to their tuple type + structure. + \end{descr}