src/Provers/classical.ML
changeset 9941 fe05af7ec816
parent 9938 cb6a7572d0a1
child 9952 24914e42b857
--- a/src/Provers/classical.ML	Tue Sep 12 19:03:13 2000 +0200
+++ b/src/Provers/classical.ML	Tue Sep 12 22:13:23 2000 +0200
@@ -1046,10 +1046,11 @@
 
 (* setup_attrs *)
 
-fun elimified x = Attrib.no_args (Drule.rule_attribute (K Data.make_elim)) x;
+fun elim_format x = Attrib.no_args (Drule.rule_attribute (K Data.make_elim)) x;
 
 val setup_attrs = Attrib.add_attributes
- [("elimified", (elimified, elimified), "destruct rule turned into elimination rule (classical)"),
+ [("elim_format", (elim_format, elim_format),
+    "destruct rule turned into elimination rule format (classical)"),
   (destN, cla_attr (op addXDs) (op addDs) (op addSDs), "declaration of destruction rule"),
   (elimN, cla_attr (op addXEs) (op addEs) (op addSEs), "declaration of elimination rule"),
   (introN, cla_attr (op addXIs) (op addIs) (op addSIs), "declaration of introduction rule"),