equal
deleted
inserted
replaced
36 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = |
36 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = |
37 struct |
37 struct |
38 |
38 |
39 fun plural_s n = if n = 1 then "" else "s" |
39 fun plural_s n = if n = 1 then "" else "s" |
40 |
40 |
41 fun serial_commas _ [] = ["??"] |
41 val serial_commas = ATP_Proof.serial_commas |
42 | serial_commas _ [s] = [s] |
|
43 | serial_commas conj [s1, s2] = [s1, conj, s2] |
|
44 | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3] |
|
45 | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss |
|
46 |
|
47 val simplify_spaces = ATP_Proof.strip_spaces false (K true) |
42 val simplify_spaces = ATP_Proof.strip_spaces false (K true) |
48 |
43 |
49 fun parse_bool_option option name s = |
44 fun parse_bool_option option name s = |
50 (case s of |
45 (case s of |
51 "smart" => if option then NONE else raise Option |
46 "smart" => if option then NONE else raise Option |