author | wenzelm |
Thu, 22 Dec 2005 00:28:36 +0100 | |
changeset 18457 | 356a9f711899 |
parent 18449 | e314fb38307d |
child 18794 | 46d66332bf81 |
permissions | -rw-r--r-- |
15151 | 1 |
(* Title: HOL/Reconstruction.thy |
17603 | 2 |
ID: $Id$ |
15151 | 3 |
Author: Lawrence C Paulson |
4 |
Copyright 2004 University of Cambridge |
|
5 |
*) |
|
6 |
||
17462
47f7bddc3239
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
wenzelm
parents:
17421
diff
changeset
|
7 |
header{* Reconstructing external resolution proofs *} |
15151 | 8 |
|
9 |
theory Reconstruction |
|
17508 | 10 |
imports Hilbert_Choice Map Infinite_Set Extraction |
18449 | 11 |
uses "Tools/polyhash.ML" |
12 |
"Tools/res_clause.ML" |
|
13 |
"Tools/res_hol_clause.ML" |
|
17819 | 14 |
"Tools/res_axioms.ML" |
15 |
"Tools/ATP/recon_order_clauses.ML" |
|
16 |
"Tools/ATP/recon_translate_proof.ML" |
|
17 |
"Tools/ATP/recon_parse.ML" |
|
18 |
"Tools/ATP/recon_transfer_proof.ML" |
|
19 |
"Tools/ATP/AtpCommunication.ML" |
|
20 |
"Tools/ATP/watcher.ML" |
|
21 |
"Tools/ATP/res_clasimpset.ML" |
|
22 |
"Tools/res_atp.ML" |
|
23 |
"Tools/reconstruction.ML" |
|
15151 | 24 |
|
25 |
begin |
|
26 |
||
16563 | 27 |
setup ResAxioms.meson_method_setup |
15151 | 28 |
setup Reconstruction.setup |
29 |
||
15653 | 30 |
end |