# HG changeset patch
# User wenzelm
# Date 968353018 -7200
# Node ID 8035a13c61a0f717baeb5672c940a082771e10b7
# Parent  5a9081c3b869ab250a1f3f696db1d4b67b256450
tuned msgs;

diff -r 5a9081c3b869 -r 8035a13c61a0 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Thu Sep 07 20:56:04 2000 +0200
+++ b/src/Provers/splitter.ML	Thu Sep 07 20:56:58 2000 +0200
@@ -430,7 +430,7 @@
 (** theory setup **)
 
 val setup =
- [Attrib.add_attributes [(splitN, split_attr, "declare splitter rule")],
-  Method.add_methods [(splitN, split_meth oo split_args, "apply splitter rule")]];
+ [Attrib.add_attributes [(splitN, split_attr, "declaration of case split rule")],
+  Method.add_methods [(splitN, split_meth oo split_args, "apply case split rule")]];
 
 end;
diff -r 5a9081c3b869 -r 8035a13c61a0 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Thu Sep 07 20:56:04 2000 +0200
+++ b/src/Pure/Isar/calculation.ML	Thu Sep 07 20:56:58 2000 +0200
@@ -177,7 +177,7 @@
 (** theory setup **)
 
 val setup = [GlobalCalculation.init, LocalCalculation.init,
-  Attrib.add_attributes [("trans", trans_attr, "declare transitivity rule")]];
+  Attrib.add_attributes [("trans", trans_attr, "declaration of transitivity rule")]];
 
 
 end;
diff -r 5a9081c3b869 -r 8035a13c61a0 src/Pure/Isar/method.ML
--- 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")];