--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Dec 20 15:51:24 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Dec 20 15:51:27 2012 +0100
@@ -7,6 +7,7 @@
signature SLEDGEHAMMER_UTIL =
sig
val sledgehammerN : string
+ val log2 : real -> real
val plural_s : int -> string
val serial_commas : string -> string list -> string list
val simplify_spaces : string -> string
@@ -32,6 +33,10 @@
val sledgehammerN = "sledgehammer"
+val log10_2 = Math.log10 2.0
+
+fun log2 n = Math.log10 n / log10_2
+
fun plural_s n = if n = 1 then "" else "s"
val serial_commas = Try.serial_commas