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 Map Infinite_Set Extraction |
10 imports Hilbert_Choice Map Infinite_Set Extraction |
11 files "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 |