# HG changeset patch
# User wenzelm
# Date 1138559020 -3600
# Node ID bead1a4e966b30a6dcdf306295c113ede1954734
# Parent  6ab4de872a7028fa9b94ff110014096cd29049f1
tuned comment;

diff -r 6ab4de872a70 -r bead1a4e966b src/HOL/Tools/res_axioms.ML
--- 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")];
 
 
 
diff -r 6ab4de872a70 -r bead1a4e966b src/Provers/eqsubst.ML
--- 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;