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