src/HOL/Reconstruction.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 18794 46d66332bf81
child 19767 6e77bd331bf4
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     1 (*  Title:      HOL/Reconstruction.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson
     4     Copyright   2004  University of Cambridge
     5 *)
     6 
     7 header{* Reconstructing external resolution proofs *}
     8 
     9 theory Reconstruction
    10 imports Hilbert_Choice Map Infinite_Set Extraction
    11 uses 	 "Tools/polyhash.ML"
    12          "Tools/res_clause.ML"
    13 	 "Tools/res_hol_clause.ML"
    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/reduce_axiomsN.ML"
    22 	 "Tools/ATP/res_clasimpset.ML"
    23 	 "Tools/res_atp.ML"
    24 	 "Tools/reconstruction.ML"
    25 
    26 begin
    27 
    28 setup ResAxioms.meson_method_setup
    29 setup Reconstruction.setup
    30 
    31 end