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