tuned message
authorblanchet
Sat, 05 Jan 2013 22:31:33 +0100
changeset 50751 d3111134973d
parent 50750 518f0b5ef3d9
child 50752 d5834be31864
tuned message
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Jan 05 22:31:32 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Jan 05 22:31:33 2013 +0100
@@ -866,7 +866,7 @@
         " proofs to learn." ^
         (if auto_level = 0 andalso not run_prover then
            "\n\nHint: Try " ^ sendback learn_proverN ^
-           " to learn from automatic provers."
+           " to learn from an automatic prover."
          else
            "")
       else