equal
deleted
inserted
replaced
4 General-purpose functions used by the Sledgehammer modules. |
4 General-purpose functions used by the Sledgehammer modules. |
5 *) |
5 *) |
6 |
6 |
7 signature SLEDGEHAMMER_UTIL = |
7 signature SLEDGEHAMMER_UTIL = |
8 sig |
8 sig |
|
9 val sledgehammerN : string |
9 val plural_s : int -> string |
10 val plural_s : int -> string |
10 val serial_commas : string -> string list -> string list |
11 val serial_commas : string -> string list -> string list |
11 val simplify_spaces : string -> string |
12 val simplify_spaces : string -> string |
12 val infinite_timeout : Time.time |
13 val infinite_timeout : Time.time |
13 val time_mult : real -> Time.time -> Time.time |
14 val time_mult : real -> Time.time -> Time.time |
20 |
21 |
21 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = |
22 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = |
22 struct |
23 struct |
23 |
24 |
24 open ATP_Util |
25 open ATP_Util |
|
26 |
|
27 val sledgehammerN = "sledgehammer" |
25 |
28 |
26 fun plural_s n = if n = 1 then "" else "s" |
29 fun plural_s n = if n = 1 then "" else "s" |
27 |
30 |
28 val serial_commas = Try.serial_commas |
31 val serial_commas = Try.serial_commas |
29 val simplify_spaces = strip_spaces false (K true) |
32 val simplify_spaces = strip_spaces false (K true) |