equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 signature SLEDGEHAMMER_UTIL = |
7 signature SLEDGEHAMMER_UTIL = |
8 sig |
8 sig |
9 val sledgehammerN : string |
9 val sledgehammerN : string |
|
10 val log2 : real -> real |
10 val plural_s : int -> string |
11 val plural_s : int -> string |
11 val serial_commas : string -> string list -> string list |
12 val serial_commas : string -> string list -> string list |
12 val simplify_spaces : string -> string |
13 val simplify_spaces : string -> string |
13 val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b |
14 val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b |
14 val infinite_timeout : Time.time |
15 val infinite_timeout : Time.time |
29 struct |
30 struct |
30 |
31 |
31 open ATP_Util |
32 open ATP_Util |
32 |
33 |
33 val sledgehammerN = "sledgehammer" |
34 val sledgehammerN = "sledgehammer" |
|
35 |
|
36 val log10_2 = Math.log10 2.0 |
|
37 |
|
38 fun log2 n = Math.log10 n / log10_2 |
34 |
39 |
35 fun plural_s n = if n = 1 then "" else "s" |
40 fun plural_s n = if n = 1 then "" else "s" |
36 |
41 |
37 val serial_commas = Try.serial_commas |
42 val serial_commas = Try.serial_commas |
38 val simplify_spaces = strip_spaces false (K true) |
43 val simplify_spaces = strip_spaces false (K true) |