equal
deleted
inserted
replaced
15 ML {* |
15 ML {* |
16 val (time, ((type_map, const_map, fmlas), thy)) = |
16 val (time, ((type_map, const_map, fmlas), thy)) = |
17 Timing.timing |
17 Timing.timing |
18 (TPTP_Interpret.interpret_file |
18 (TPTP_Interpret.interpret_file |
19 false |
19 false |
20 (Path.dir tptp_probs_dir) |
20 [Path.explode "$TPTP"] |
21 (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p")) |
21 (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p")) |
22 [] |
22 [] |
23 []) |
23 []) |
24 @{theory} |
24 @{theory} |
25 *} |
25 *} |
36 (*default timeout is 1 min*) |
36 (*default timeout is 1 min*) |
37 fun interpret timeout file thy = |
37 fun interpret timeout file thy = |
38 TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout)) |
38 TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout)) |
39 (TPTP_Interpret.interpret_file |
39 (TPTP_Interpret.interpret_file |
40 false |
40 false |
41 (Path.dir tptp_probs_dir) |
41 [Path.explode "$TPTP"] |
42 file |
42 file |
43 [] |
43 [] |
44 []) thy |
44 []) thy |
45 |
45 |
46 fun interpret_timed timeout file thy = |
46 fun interpret_timed timeout file thy = |