src/HOL/Reconstruction.thy
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 18794 46d66332bf81
child 19767 6e77bd331bf4
permissions -rw-r--r--
adaptions to codegen_package
paulson@15151
     1
(*  Title:      HOL/Reconstruction.thy
webertj@17603
     2
    ID:         $Id$
paulson@15151
     3
    Author:     Lawrence C Paulson
paulson@15151
     4
    Copyright   2004  University of Cambridge
paulson@15151
     5
*)
paulson@15151
     6
wenzelm@17462
     7
header{* Reconstructing external resolution proofs *}
paulson@15151
     8
paulson@15151
     9
theory Reconstruction
wenzelm@17508
    10
imports Hilbert_Choice Map Infinite_Set Extraction
paulson@18449
    11
uses 	 "Tools/polyhash.ML"
paulson@18449
    12
         "Tools/res_clause.ML"
paulson@18449
    13
	 "Tools/res_hol_clause.ML"
paulson@17819
    14
	 "Tools/res_axioms.ML"
paulson@17819
    15
	 "Tools/ATP/recon_order_clauses.ML"
paulson@17819
    16
	 "Tools/ATP/recon_translate_proof.ML"
paulson@17819
    17
	 "Tools/ATP/recon_parse.ML"
paulson@17819
    18
	 "Tools/ATP/recon_transfer_proof.ML"
paulson@17819
    19
	 "Tools/ATP/AtpCommunication.ML"
paulson@17819
    20
	 "Tools/ATP/watcher.ML"
mengj@18794
    21
         "Tools/ATP/reduce_axiomsN.ML"
paulson@17819
    22
	 "Tools/ATP/res_clasimpset.ML"
paulson@17819
    23
	 "Tools/res_atp.ML"
paulson@17819
    24
	 "Tools/reconstruction.ML"
paulson@15151
    25
paulson@15151
    26
begin
paulson@15151
    27
paulson@16563
    28
setup ResAxioms.meson_method_setup
paulson@15151
    29
setup Reconstruction.setup
paulson@15151
    30
quigley@15653
    31
end