--- a/src/HOL/Tools/res_axioms.ML Sun Jan 29 19:23:38 2006 +0100
+++ b/src/HOL/Tools/res_axioms.ML Sun Jan 29 19:23:40 2006 +0100
@@ -473,7 +473,7 @@
val meson_method_setup =
Method.add_methods
[("meson", Method.thms_ctxt_args meson_meth,
- "The MESON resolution proof procedure")];
+ "MESON resolution proof procedure")];
--- a/src/Provers/eqsubst.ML Sun Jan 29 19:23:38 2006 +0100
+++ b/src/Provers/eqsubst.ML Sun Jan 29 19:23:40 2006 +0100
@@ -337,6 +337,6 @@
val setup =
- Method.add_method ("subst", subst_meth, "substiution with an equation");
+ Method.add_method ("subst", subst_meth, "single-step substitution");
end;