# HG changeset patch
# User wenzelm
# Date 953403528 -3600
# Node ID 981f52707e5d8b3c14fe6c8afbf72bf8443c8ee3
# Parent  daaedc7b56a9dc4cd2a9e7d460e8697748af9e06
tuned comments;

diff -r daaedc7b56a9 -r 981f52707e5d src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat Mar 18 19:16:56 2000 +0100
+++ b/src/Provers/classical.ML	Sat Mar 18 19:18:48 2000 +0100
@@ -1040,7 +1040,7 @@
  [(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")];
+  (delruleN, del_attr, "undeclare rule")];
 
 
 
diff -r daaedc7b56a9 -r 981f52707e5d src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sat Mar 18 19:16:56 2000 +0100
+++ b/src/Pure/Isar/method.ML	Sat Mar 18 19:18:48 2000 +0100
@@ -187,10 +187,10 @@
 (* concrete syntax *)
 
 val rule_atts =
- [("dest", (Attrib.no_args dest_global, Attrib.no_args dest_local), "destruction rule"),
-  ("elim", (Attrib.no_args elim_global, Attrib.no_args elim_local), "elimination rule"),
-  ("intro", (Attrib.no_args intro_global, Attrib.no_args intro_local), "introduction rule"),
-  ("delrule", (Attrib.no_args delrule_global, Attrib.no_args delrule_local), "delete rule")];
+ [("dest", (Attrib.no_args dest_global, Attrib.no_args dest_local), "declare destruction rule"),
+  ("elim", (Attrib.no_args elim_global, Attrib.no_args elim_local), "declare elimination rule"),
+  ("intro", (Attrib.no_args intro_global, Attrib.no_args intro_local), "declare introduction rule"),
+  ("delrule", (Attrib.no_args delrule_global, Attrib.no_args delrule_local), "undeclare rule")];