src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
changeset 54140 564b8adb0952
parent 54131 18b23d787062
child 54141 f57f8e7a879f
--- 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