src/HOL/Reconstruction.thy
author haftmann
Mon Aug 14 13:46:06 2006 +0200 (2006-08-14)
changeset 20380 14f9f2a1caa6
parent 19767 6e77bd331bf4
child 20761 7a6f69cf5a86
permissions -rw-r--r--
simplified code generator setup
     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/res_atp.ML"
    23 	 "Tools/reconstruction.ML"
    24 
    25 begin
    26 
    27 setup ResAxioms.meson_method_setup
    28 setup Reconstruction.setup
    29 
    30 end