# HG changeset patch
# User blanchet
# Date 1382034053 -7200
# Node ID 564b8adb095275fb94c8f2e59fd1d74186cafaef
# Parent  c8ea98c1f4b2da7c30fd835d6cabce58bccf9346
clarified message

diff -r c8ea98c1f4b2 -r 564b8adb0952 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Oct 17 20:03:37 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Oct 17 20:20:53 2013 +0200
@@ -1201,7 +1201,7 @@
       in
         if verbose orelse auto_level < 2 then
           "Learned " ^ string_of_int n ^ " nontrivial " ^
-          (if run_prover then "automatic" else "Isar") ^ " proof" ^ plural_s n ^
+          (if run_prover then "automatic and " else "") ^ "Isar proof" ^ plural_s n ^
           (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer)
            else "") ^ "."
         else