Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
used standard Time.compare in Sledgehammer's preplay
authordesharna
Mon, 02 Oct 2023 11:22:53 +0200
changeset 78736 45867a453a3f
parent 78735 a0f85118488c
child 78737 183a28459663
used standard Time.compare in Sledgehammer's preplay
src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Fri Sep 29 17:22:19 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Mon Oct 02 11:22:53 2023 +0200
@@ -160,12 +160,10 @@
     if time = Time.zeroTime then "" else string_of_ext_time (true, time) ^ ", timed out"
   | string_of_play_outcome Play_Failed = "failed"
 
-fun play_outcome_ord (Played time1, Played time2) =
-    int_ord (apply2 Time.toMilliseconds (time1, time2))
+fun play_outcome_ord (Played time1, Played time2) = Time.compare (time1, time2)
   | play_outcome_ord (Played _, _) = LESS
   | play_outcome_ord (_, Played _) = GREATER
-  | play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) =
-    int_ord (apply2 Time.toMilliseconds (time1, time2))
+  | play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) = Time.compare (time1, time2)
   | play_outcome_ord (Play_Timed_Out _, _) = LESS
   | play_outcome_ord (_, Play_Timed_Out _) = GREATER
   | play_outcome_ord (Play_Failed, Play_Failed) = EQUAL
isabelle