# HG changeset patch
# User wenzelm
# Date 968772890 -7200
# Node ID f080397656d8e2f91d2e7afbc68a6a9546c32563
# Parent  a87965201c345f82aa1c0299ce4d0a95fa36b0ee
renamed "delrule" to "rule del";

diff -r a87965201c34 -r f080397656d8 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Tue Sep 12 17:34:41 2000 +0200
+++ b/doc-src/IsarRef/generic.tex	Tue Sep 12 17:34:50 2000 +0200
@@ -321,7 +321,7 @@
   folded & : & \isaratt \\[0.5ex]
   standard & : & \isaratt \\
   elimified & : & \isaratt \\
-  no_vars & : & \isaratt \\
+  no_vars^* & : & \isaratt \\
   exported^* & : & \isaratt \\
 \end{matharray}
 
@@ -787,20 +787,23 @@
 
 \indexisarcmd{print-claset}
 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
-\indexisaratt{iff}\indexisaratt{delrule}
+\indexisaratt{iff}\indexisaratt{rule}
 \begin{matharray}{rcl}
   print_claset & : & \isarkeep{theory~|~proof} \\
   intro & : & \isaratt \\
   elim & : & \isaratt \\
   dest & : & \isaratt \\
+  rule & : & \isaratt \\
   iff & : & \isaratt \\
-  delrule & : & \isaratt \\
 \end{matharray}
 
 \begin{rail}
   ('intro' | 'elim' | 'dest') ('!' | () | '?')
   ;
+  'rule' 'del'
+  ;
   'iff' (() | 'add' | 'del')
+  ;
 \end{rail}
 
 \begin{descr}
@@ -813,13 +816,10 @@
   single ``!'' classifies as \emph{safe}, and ``?'' as \emph{extra} (i.e.\ not
   applied in the search-oriented automated methods, but only in single-step
   methods such as $rule$).
-
+\item [$rule~del$] deletes introduction, elimination, or destruct rules from
+  the context.
 \item [$iff$] declares equations both as rules for the Simplifier and
   Classical Reasoner.
-
-\item [$delrule$] deletes introduction or elimination rules from the context.
-  Note that destruction rules would have to be turned into elimination rules
-  first, e.g.\ by using the $elimified$ attribute.
 \end{descr}
 
 
diff -r a87965201c34 -r f080397656d8 doc-src/IsarRef/pure.tex
--- 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}