--- a/src/Pure/Isar/method.ML Thu Sep 07 20:56:04 2000 +0200
+++ b/src/Pure/Isar/method.ML Thu Sep 07 20:56:58 2000 +0200
@@ -203,10 +203,14 @@
(* concrete syntax *)
val rule_atts =
- [("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")];
+ [("dest", (Attrib.no_args dest_global, Attrib.no_args dest_local),
+ "declaration of destruction rule"),
+ ("elim", (Attrib.no_args elim_global, Attrib.no_args elim_local),
+ "declaration of elimination rule"),
+ ("intro", (Attrib.no_args intro_global, Attrib.no_args intro_local),
+ "declaration of introduction rule"),
+ ("delrule", (Attrib.no_args delrule_global, Attrib.no_args delrule_local),
+ "remove declaration of elim/intro rule")];