# 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