doc-src/IsarRef/hol.tex
changeset 11039 55de839f4850
parent 10802 7fa042e28c43
child 11051 00b70f3196c2
     1.1 --- a/doc-src/IsarRef/hol.tex	Fri Feb 02 22:21:06 2001 +0100
     1.2 +++ b/doc-src/IsarRef/hol.tex	Fri Feb 02 23:59:30 2001 +0100
     1.3 @@ -3,17 +3,24 @@
     1.4  
     1.5  \section{Miscellaneous attributes}\label{sec:rule-format}
     1.6  
     1.7 -\indexisaratt{rule-format}
     1.8 +\indexisaratt{rule-format}\indexisaratt{split-format}
     1.9  \begin{matharray}{rcl}
    1.10    rule_format & : & \isaratt \\
    1.11 +  split_format & : & \isaratt \\
    1.12  \end{matharray}
    1.13  
    1.14  \railalias{ruleformat}{rule\_format}
    1.15  \railterm{ruleformat}
    1.16  
    1.17 +\railalias{splitformat}{split\_format}
    1.18 +\railterm{splitformat}
    1.19 +\railterm{complete}
    1.20 +
    1.21  \begin{rail}
    1.22    ruleformat ('(' noasm ')')?
    1.23    ;
    1.24 +  splitformat (((name * ) + 'and') | ('(' complete ')'))
    1.25 +  ;
    1.26  \end{rail}
    1.27  
    1.28  \begin{descr}
    1.29 @@ -23,6 +30,15 @@
    1.30    the corresponding meta-logical connectives.  By default, the result is fully
    1.31    normalized, including assumptions and conclusions at any depth.  The
    1.32    $no_asm$ option restricts the transformation to the conclusion of a rule.
    1.33 +  
    1.34 +\item [$split_format~\vec p@1 \dots \vec p@n$] puts tuple objects into
    1.35 +  canonical form as specified by the arguments given; $\vec p@i$ refers to
    1.36 +  occurrences in premise $i$ of the rule.
    1.37 +  
    1.38 +  The $split_format~(complete)$ form causes \emph{all} arguments in function
    1.39 +  applications to be represented canonically according to their tuple type
    1.40 +  structure.
    1.41 +
    1.42  \end{descr}
    1.43  
    1.44