# HG changeset patch
# User wenzelm
# Date 962219702 -7200
# Node ID c6c5b422241f883042e3af2677c4cb469045a1d4
# Parent  cd4494dc789a3e9271d51f02f0ec056d56fabcbd
classical 'elimify' attribute;

diff -r cd4494dc789a -r c6c5b422241f src/Provers/classical.ML
--- a/src/Provers/classical.ML	Wed Jun 28 19:57:16 2000 +0200
+++ b/src/Provers/classical.ML	Wed Jun 28 21:15:02 2000 +0200
@@ -1038,8 +1038,11 @@
 
 (* setup_attrs *)
 
+fun elimify x = Attrib.no_args (Drule.rule_attribute (K make_elim)) x;
+
 val setup_attrs = Attrib.add_attributes
- [(destN, cla_attr (op addXDs) (op addDs) (op addSDs), "declare destruction rule"),
+ [("elimify", (elimify, elimify), "turn destruct rule into elimination rule (classical)"),
+  (destN, cla_attr (op addXDs) (op addDs) (op addSDs), "declare destruction rule"),
   (elimN, cla_attr (op addXEs) (op addEs) (op addSEs), "declare elimination rule"),
   (introN, cla_attr (op addXIs) (op addIs) (op addSIs), "declare introduction rule"),
   (delruleN, del_attr, "undeclare rule")];