--- 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")];