doc-src/IsarRef/pure.tex
changeset 9936 f080397656d8
parent 9727 5e18de753e0f
child 10160 bb8f9412fec6
     1.1 --- a/doc-src/IsarRef/pure.tex	Tue Sep 12 17:34:41 2000 +0200
     1.2 +++ b/doc-src/IsarRef/pure.tex	Tue Sep 12 17:34:50 2000 +0200
     1.3 @@ -845,7 +845,7 @@
     1.4  \ref{ch:hol-tools}).
     1.5  
     1.6  \indexisarmeth{assumption}\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{$-$}
     1.7 -\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
     1.8 +\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}\indexisaratt{rule}
     1.9  \indexisaratt{OF}\indexisaratt{of}
    1.10  \begin{matharray}{rcl}
    1.11    assumption & : & \isarmeth \\
    1.12 @@ -857,7 +857,7 @@
    1.13    intro & : & \isaratt \\
    1.14    elim & : & \isaratt \\
    1.15    dest & : & \isaratt \\
    1.16 -  delrule & : & \isaratt \\
    1.17 +  rule & : & \isaratt \\
    1.18  \end{matharray}
    1.19  
    1.20  \begin{rail}
    1.21 @@ -867,6 +867,8 @@
    1.22    ;
    1.23    'of' insts ('concl' ':' insts)?
    1.24    ;
    1.25 +  'rule' 'del'
    1.26 +  ;
    1.27  \end{rail}
    1.28  
    1.29  \begin{descr}
    1.30 @@ -906,7 +908,7 @@
    1.31    attributes, and the $rule$ method, too.  In object-logics with classical
    1.32    reasoning enabled, the latter version should be used all the time to avoid
    1.33    confusion!
    1.34 -\item [$delrule$] undeclares introduction or elimination rules.
    1.35 +\item [$rule~del$] undeclares introduction, elimination, or destruct rules.
    1.36  \end{descr}
    1.37  
    1.38