equal
deleted
inserted
replaced
42 type ('a, 'b) atp_step = |
42 type ('a, 'b) atp_step = |
43 atp_step_name * atp_formula_role * 'a * 'b * atp_step_name list |
43 atp_step_name * atp_formula_role * 'a * 'b * atp_step_name list |
44 |
44 |
45 type 'a atp_proof = (('a, 'a, ('a, 'a atp_type) atp_term, 'a) atp_formula, string) atp_step list |
45 type 'a atp_proof = (('a, 'a, ('a, 'a atp_type) atp_term, 'a) atp_formula, string) atp_step list |
46 |
46 |
47 (* Named ATPs *) |
|
48 val agsyholN : string |
47 val agsyholN : string |
49 val alt_ergoN : string |
48 val alt_ergoN : string |
50 val eN : string |
49 val eN : string |
51 val e_parN : string |
|
52 val iproverN : string |
50 val iproverN : string |
53 val leo2N : string |
51 val leo2N : string |
54 val leo3N : string |
52 val leo3N : string |
55 val pirateN : string |
53 val pirateN : string |
56 val satallaxN : string |
54 val satallaxN : string |
57 val snarkN : string |
|
58 val spassN : string |
55 val spassN : string |
59 val vampireN : string |
56 val vampireN : string |
60 val waldmeisterN : string |
57 val waldmeisterN : string |
61 val z3_tptpN : string |
58 val z3_tptpN : string |
62 val zipperpositionN : string |
59 val zipperpositionN : string |
107 struct |
104 struct |
108 |
105 |
109 open ATP_Util |
106 open ATP_Util |
110 open ATP_Problem |
107 open ATP_Problem |
111 |
108 |
112 (* Named ATPs *) |
|
113 |
|
114 val agsyholN = "agsyhol" |
109 val agsyholN = "agsyhol" |
115 val alt_ergoN = "alt_ergo" |
110 val alt_ergoN = "alt_ergo" |
116 val eN = "e" |
111 val eN = "e" |
117 val e_parN = "e_par" |
|
118 val iproverN = "iprover" |
112 val iproverN = "iprover" |
119 val leo2N = "leo2" |
113 val leo2N = "leo2" |
120 val leo3N = "leo3" |
114 val leo3N = "leo3" |
121 val pirateN = "pirate" |
115 val pirateN = "pirate" |
122 val satallaxN = "satallax" |
116 val satallaxN = "satallax" |
123 val snarkN = "snark" |
|
124 val spassN = "spass" |
117 val spassN = "spass" |
125 val vampireN = "vampire" |
118 val vampireN = "vampire" |
126 val waldmeisterN = "waldmeister" |
119 val waldmeisterN = "waldmeister" |
127 val z3_tptpN = "z3_tptp" |
120 val z3_tptpN = "z3_tptp" |
128 val zipperpositionN = "zipperposition" |
121 val zipperpositionN = "zipperposition" |