# HG changeset patch
# User wenzelm
# Date 953142060 -3600
# Node ID f06fc940c61c05ed2ed96de1f2490bf75dd33140
# Parent  482c301041b495982784fdfe4b9679c3426cd3de
tuned comments;

diff -r 482c301041b4 -r f06fc940c61c src/Provers/classical.ML
--- a/src/Provers/classical.ML	Wed Mar 15 18:40:03 2000 +0100
+++ b/src/Provers/classical.ML	Wed Mar 15 18:41:00 2000 +0100
@@ -1037,9 +1037,9 @@
 (* setup_attrs *)
 
 val setup_attrs = Attrib.add_attributes
- [(destN, cla_attr (op addXDs) (op addDs) (op addSDs), "destruction rule"),
-  (elimN, cla_attr (op addXEs) (op addEs) (op addSEs), "elimination rule"),
-  (introN, cla_attr (op addXIs) (op addIs) (op addSIs), "introduction rule"),
+ [(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, "delete rule")];