equal
deleted
inserted
replaced
29 |
29 |
30 (* wrapper for calling external prover *) |
30 (* wrapper for calling external prover *) |
31 |
31 |
32 fun string_for_failure Unprovable = "Unprovable." |
32 fun string_for_failure Unprovable = "Unprovable." |
33 | string_for_failure TimedOut = "Timed out." |
33 | string_for_failure TimedOut = "Timed out." |
|
34 | string_for_failure Interrupted = "Interrupted." |
34 | string_for_failure _ = "Unknown error." |
35 | string_for_failure _ = "Unknown error." |
35 |
36 |
36 fun n_theorems names = |
37 fun n_theorems names = |
37 let val n = length names in |
38 let val n = length names in |
38 string_of_int n ^ " theorem" ^ plural_s n ^ |
39 string_of_int n ^ " theorem" ^ plural_s n ^ |