author | blanchet |
Tue, 14 Sep 2010 19:40:19 +0200 | |
changeset 39371 | 6549ca3671f3 |
parent 39370 | f8292d3020db |
child 39372 | 2fd8a9a7080d |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Sep 14 19:38:44 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Sep 14 19:40:19 2010 +0200 @@ -356,7 +356,8 @@ subgoal) |>> (fn message => message ^ (if verbose then - "\nReal CPU time: " ^ string_of_int msecs ^ " ms." + "\nATP real CPU time: " ^ string_of_int msecs ^ + " ms." else "") ^ (if important_message <> "" then