# HG changeset patch
# User wenzelm
# Date 1235828574 -3600
# Node ID 9321f7b70450e394dbe770aecea9557949186817
# Parent  faf95eb3f3759475a167c3be1d312d3d68daca06
tuned message;

diff -r faf95eb3f375 -r 9321f7b70450 src/Tools/coherent.ML
--- a/src/Tools/coherent.ML	Sat Feb 28 14:17:44 2009 +0100
+++ b/src/Tools/coherent.ML	Sat Feb 28 14:42:54 2009 +0100
@@ -228,6 +228,6 @@
   Method.METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1);
 
 val setup = Method.add_method
-  ("coherent", Method.thms_ctxt_args coherent_meth, "Prove coherent formula");
+  ("coherent", Method.thms_ctxt_args coherent_meth, "prove coherent formula");
 
 end;