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