equal
deleted
inserted
replaced
6 |
6 |
7 header{*Attributes for Reconstructing External Resolution Proofs*} |
7 header{*Attributes for Reconstructing External Resolution Proofs*} |
8 |
8 |
9 theory Reconstruction |
9 theory Reconstruction |
10 imports Hilbert_Choice |
10 imports Hilbert_Choice |
11 files "Tools/reconstruction.ML" |
11 files "Tools/res_lib.ML" |
|
12 "Tools/res_clause.ML" |
|
13 "Tools/res_skolem_function.ML" |
|
14 "Tools/res_axioms.ML" |
|
15 "Tools/res_types_sorts.ML" |
|
16 "Tools/res_atp.ML" |
|
17 "Tools/reconstruction.ML" |
12 |
18 |
13 begin |
19 begin |
14 |
20 |
15 setup Reconstruction.setup |
21 setup Reconstruction.setup |
16 |
22 |