equal
deleted
inserted
replaced
5 *) |
5 *) |
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 Commutative_Ring Extraction |
11 uses "Tools/res_lib.ML" |
11 uses "Tools/res_lib.ML" |
12 |
12 |
13 "Tools/res_clause.ML" |
13 "Tools/res_clause.ML" |
14 "Tools/res_skolem_function.ML" |
14 "Tools/res_skolem_function.ML" |
15 "Tools/res_axioms.ML" |
15 "Tools/res_axioms.ML" |