doc-src/IsarRef/hol.tex
changeset 9941 fe05af7ec816
parent 9935 a87965201c34
child 9949 1741a61d4b33
     1.1 --- a/doc-src/IsarRef/hol.tex	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/doc-src/IsarRef/hol.tex	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -3,21 +3,24 @@
     1.4  
     1.5  \section{Miscellaneous attributes}
     1.6  
     1.7 -\indexisaratt{rulified}
     1.8 +\indexisaratt{rule-format}
     1.9  \begin{matharray}{rcl}
    1.10 -  rulified & : & \isaratt \\
    1.11 +  rule_format & : & \isaratt \\
    1.12  \end{matharray}
    1.13  
    1.14 +\railalias{ruleformat}{rule\_format}
    1.15 +\railterm{ruleformat}
    1.16 +
    1.17  \begin{rail}
    1.18 -  'rulified' ('(' noasm ')')?
    1.19 +  ruleformat ('(' noasm ')')?
    1.20    ;
    1.21  \end{rail}
    1.22  
    1.23  \begin{descr}
    1.24    
    1.25 -\item [$rulified$] causes a theorem to be put into standard object-rule form,
    1.26 -  replacing implication and (bounded) universal quantification of HOL by the
    1.27 -  corresponding meta-logical connectives.  By default, the result is fully
    1.28 +\item [$rule_format$] causes a theorem to be put into standard object-rule
    1.29 +  form, replacing implication and (bounded) universal quantification of HOL by
    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  \end{descr}