--- a/doc-src/IsarRef/pure.tex Tue Sep 12 17:34:41 2000 +0200
+++ b/doc-src/IsarRef/pure.tex Tue Sep 12 17:34:50 2000 +0200
@@ -845,7 +845,7 @@
\ref{ch:hol-tools}).
\indexisarmeth{assumption}\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{$-$}
-\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
+\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}\indexisaratt{rule}
\indexisaratt{OF}\indexisaratt{of}
\begin{matharray}{rcl}
assumption & : & \isarmeth \\
@@ -857,7 +857,7 @@
intro & : & \isaratt \\
elim & : & \isaratt \\
dest & : & \isaratt \\
- delrule & : & \isaratt \\
+ rule & : & \isaratt \\
\end{matharray}
\begin{rail}
@@ -867,6 +867,8 @@
;
'of' insts ('concl' ':' insts)?
;
+ 'rule' 'del'
+ ;
\end{rail}
\begin{descr}
@@ -906,7 +908,7 @@
attributes, and the $rule$ method, too. In object-logics with classical
reasoning enabled, the latter version should be used all the time to avoid
confusion!
-\item [$delrule$] undeclares introduction or elimination rules.
+\item [$rule~del$] undeclares introduction, elimination, or destruct rules.
\end{descr}