--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100
@@ -252,9 +252,12 @@
val message = message ()
val () =
- (case outcome of
- SH_Some _ => the_default writeln writeln_result (prover_name ^ ": " ^ message)
- | _ => ())
+ if mode = Auto_Try then
+ ()
+ else
+ (case outcome of
+ SH_Some _ => the_default writeln writeln_result (prover_name ^ ": " ^ message)
+ | _ => ())
in
(outcome, message)
end
@@ -452,7 +455,7 @@
|> `(fn (outcome, _) =>
(case outcome of
SH_Some _ => (print "QED"; true)
- | _ => (print "Sorry"; false)))
+ | _ => (print "No proof found"; false)))
end)
end;