author | wenzelm |
Sat, 17 Sep 2005 18:11:22 +0200 | |
changeset 17462 | 47f7bddc3239 |
parent 17421 | 0382f6877b98 |
child 17484 | f6a225f97f0a |
permissions | -rw-r--r-- |
15151 | 1 |
(* Title: HOL/Reconstruction.thy |
2 |
ID: $Id$ |
|
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 |
|
17462
47f7bddc3239
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
wenzelm
parents:
17421
diff
changeset
|
10 |
imports Hilbert_Choice Map Infinite_Set Commutative_Ring Extraction |
47f7bddc3239
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
wenzelm
parents:
17421
diff
changeset
|
11 |
uses "Tools/res_lib.ML" |
17236 | 12 |
|
17462
47f7bddc3239
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
wenzelm
parents:
17421
diff
changeset
|
13 |
"Tools/res_clause.ML" |
47f7bddc3239
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
wenzelm
parents:
17421
diff
changeset
|
14 |
"Tools/res_skolem_function.ML" |
47f7bddc3239
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
wenzelm
parents:
17421
diff
changeset
|
15 |
"Tools/res_axioms.ML" |
47f7bddc3239
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
wenzelm
parents:
17421
diff
changeset
|
16 |
"Tools/res_types_sorts.ML" |
15653 | 17 |
|
17462
47f7bddc3239
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
wenzelm
parents:
17421
diff
changeset
|
18 |
"Tools/ATP/recon_prelim.ML" |
47f7bddc3239
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
wenzelm
parents:
17421
diff
changeset
|
19 |
"Tools/ATP/recon_order_clauses.ML" |
47f7bddc3239
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
wenzelm
parents:
17421
diff
changeset
|
20 |
"Tools/ATP/recon_translate_proof.ML" |
47f7bddc3239
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
wenzelm
parents:
17421
diff
changeset
|
21 |
"Tools/ATP/recon_parse.ML" |
47f7bddc3239
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
wenzelm
parents:
17421
diff
changeset
|
22 |
"Tools/ATP/recon_transfer_proof.ML" |
47f7bddc3239
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
wenzelm
parents:
17421
diff
changeset
|
23 |
"Tools/ATP/VampCommunication.ML" |
47f7bddc3239
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
wenzelm
parents:
17421
diff
changeset
|
24 |
"Tools/ATP/SpassCommunication.ML" |
47f7bddc3239
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
wenzelm
parents:
17421
diff
changeset
|
25 |
"Tools/ATP/watcher.ML" |
47f7bddc3239
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
wenzelm
parents:
17421
diff
changeset
|
26 |
"Tools/ATP/res_clasimpset.ML" |
47f7bddc3239
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
wenzelm
parents:
17421
diff
changeset
|
27 |
"Tools/res_atp.ML" |
47f7bddc3239
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
wenzelm
parents:
17421
diff
changeset
|
28 |
"Tools/reconstruction.ML" |
15151 | 29 |
|
30 |
begin |
|
31 |
||
16563 | 32 |
setup ResAxioms.meson_method_setup |
15151 | 33 |
setup Reconstruction.setup |
34 |
||
15653 | 35 |
end |