# HG changeset patch
# User desharna
# Date 1741079729 -3600
# Node ID 3e972fc58373ef1089e223554d656c29836d52c1
# Parent  067dac998c59a35984aded0542dec49c19eebede
tuned success rate output of Mirabelle's sledgehammer action

diff -r 067dac998c59 -r 3e972fc58373 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Tue Mar 04 09:55:11 2025 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Tue Mar 04 10:15:29 2025 +0100
@@ -94,7 +94,7 @@
 
 val str = string_of_int
 val str3 = Real.fmt (StringCvt.FIX (SOME 3))
-fun percentage a b = string_of_int (a * 100 div b)
+fun percentage a b = Real.fmt (StringCvt.FIX (SOME 1)) (Real.fromInt (a * 100) / Real.fromInt b)
 fun ms t = Real.fromInt t / 1000.0
 fun avg_time t n =
   if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0