author | blanchet |
Thu, 28 Aug 2014 17:25:56 +0200 | |
changeset 58086 | f9ff405162a1 |
parent 58085 | ee65e9cfe284 |
child 58087 | 32d3fa94ebb4 |
--- a/src/HOL/Tools/ATP/atp_util.ML Thu Aug 28 16:58:27 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Thu Aug 28 17:25:56 2014 +0200 @@ -148,7 +148,7 @@ (if plus then "> " else "") ^ (if us < 1000 then signed_string_of_int us ^ " \<mu>s" else if us < 1000000 then signed_string_of_int (us div 1000) ^ " ms" - else string_of_real (0.1 * Real.fromInt (us div 10000)) ^ " s") + else string_of_real (0.1 * Real.fromInt (us div 100000)) ^ " s") end val string_of_time = string_of_ext_time o pair false