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