# 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}