src/Provers/classical.ML
changeset 9899 5a9081c3b869
parent 9806 98bb27b84363
child 9938 cb6a7572d0a1
     1.1 --- a/src/Provers/classical.ML	Thu Sep 07 20:55:18 2000 +0200
     1.2 +++ b/src/Provers/classical.ML	Thu Sep 07 20:56:04 2000 +0200
     1.3 @@ -1041,14 +1041,14 @@
     1.4  
     1.5  (* setup_attrs *)
     1.6  
     1.7 -fun elimify x = Attrib.no_args (Drule.rule_attribute (K make_elim)) x;
     1.8 +fun elimified x = Attrib.no_args (Drule.rule_attribute (K make_elim)) x;
     1.9  
    1.10  val setup_attrs = Attrib.add_attributes
    1.11 - [("elimify", (elimify, elimify), "turn destruct rule into elimination rule (classical)"),
    1.12 -  (destN, cla_attr (op addXDs) (op addDs) (op addSDs), "declare destruction rule"),
    1.13 -  (elimN, cla_attr (op addXEs) (op addEs) (op addSEs), "declare elimination rule"),
    1.14 -  (introN, cla_attr (op addXIs) (op addIs) (op addSIs), "declare introduction rule"),
    1.15 -  (delruleN, del_attr, "undeclare rule")];
    1.16 + [("elimified", (elimified, elimified), "destruct rule turned into elimination rule (classical)"),
    1.17 +  (destN, cla_attr (op addXDs) (op addDs) (op addSDs), "declaration of destruction rule"),
    1.18 +  (elimN, cla_attr (op addXEs) (op addEs) (op addSEs), "declaration of elimination rule"),
    1.19 +  (introN, cla_attr (op addXIs) (op addIs) (op addSIs), "declaration of introduction rule"),
    1.20 +  (delruleN, del_attr, "remove declaration of elim/intro rule")];
    1.21  
    1.22  
    1.23