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 Map Infinite_Set Extraction |
10 imports Hilbert_Choice Map Infinite_Set Extraction |
11 uses "Tools/res_lib.ML" |
11 uses "Tools/res_lib.ML" |
12 "Tools/res_clause.ML" |
12 "Tools/res_clause.ML" |
13 "Tools/res_skolem_function.ML" |
13 "Tools/res_skolem_function.ML" |
14 "Tools/res_axioms.ML" |
14 "Tools/res_axioms.ML" |
15 "Tools/res_types_sorts.ML" |
15 "Tools/res_types_sorts.ML" |
16 |
16 |
17 "Tools/ATP/recon_prelim.ML" |
17 "Tools/ATP/recon_prelim.ML" |
18 "Tools/ATP/recon_order_clauses.ML" |
18 "Tools/ATP/recon_order_clauses.ML" |
19 "Tools/ATP/recon_translate_proof.ML" |
19 "Tools/ATP/recon_translate_proof.ML" |
20 "Tools/ATP/recon_parse.ML" |
20 "Tools/ATP/recon_parse.ML" |
21 "Tools/ATP/recon_transfer_proof.ML" |
21 "Tools/ATP/recon_transfer_proof.ML" |
22 "Tools/ATP/VampCommunication.ML" |
22 "Tools/ATP/VampCommunication.ML" |
23 "Tools/ATP/VampireCommunication.ML" |
23 "Tools/ATP/VampireCommunication.ML" |
24 "Tools/ATP/SpassCommunication.ML" |
24 "Tools/ATP/SpassCommunication.ML" |
25 "Tools/ATP/watcher.sig" |
25 "Tools/ATP/watcher.sig" |
26 "Tools/ATP/watcher.ML" |
26 "Tools/ATP/watcher.ML" |
27 "Tools/ATP/res_clasimpset.ML" |
27 "Tools/ATP/res_clasimpset.ML" |
28 "Tools/res_atp.ML" |
28 "Tools/res_atp.ML" |
29 |
29 "Tools/reconstruction.ML" |
30 "Tools/reconstruction.ML" |
|
31 |
30 |
32 begin |
31 begin |
33 |
32 |
34 text{*Every theory of HOL must be a descendant or ancestor of this one!*} |
33 text{*Every theory of HOL must be a descendant or ancestor of this one!*} |
35 |
34 |