author | blanchet |
Mon, 31 Jan 2022 16:09:23 +0100 | |
changeset 75037 | 46e3a423a787 |
parent 75036 | 212e9ec706cf |
child 75038 | e5750bcb8c41 |
--- 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 @@ -423,6 +423,12 @@ if mode = Auto_Try then provers else schedule_of_provers provers slices val prover_slices = prover_slices_of_schedule ctxt params schedule + + val _ = + if verbose then + writeln ("Running " ^ commas (map fst prover_slices) ^ "...") + else + () in if mode = Auto_Try then (SH_Unknown, "")