equal
deleted
inserted
replaced
5 Reconstructors. |
5 Reconstructors. |
6 *) |
6 *) |
7 |
7 |
8 signature SLEDGEHAMMER_RECONSTRUCTOR = |
8 signature SLEDGEHAMMER_RECONSTRUCTOR = |
9 sig |
9 sig |
10 |
|
11 type stature = ATP_Problem_Generate.stature |
10 type stature = ATP_Problem_Generate.stature |
12 |
11 |
13 datatype reconstructor = |
12 datatype reconstructor = |
14 Metis of string * string | |
13 Metis of string * string | |
15 SMT |
14 SMT |
23 |
22 |
24 type one_line_params = |
23 type one_line_params = |
25 play * string * (string * stature) list * minimize_command * int * int |
24 play * string * (string * stature) list * minimize_command * int * int |
26 |
25 |
27 val smtN : string |
26 val smtN : string |
28 |
27 end; |
29 end |
|
30 |
28 |
31 structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR = |
29 structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR = |
32 struct |
30 struct |
33 |
31 |
34 open ATP_Problem_Generate |
32 open ATP_Problem_Generate |
47 type one_line_params = |
45 type one_line_params = |
48 play * string * (string * stature) list * minimize_command * int * int |
46 play * string * (string * stature) list * minimize_command * int * int |
49 |
47 |
50 val smtN = "smt" |
48 val smtN = "smt" |
51 |
49 |
52 end |
50 end; |