src/HOL/Reconstruction.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 16563 a92f96951355
child 16588 8de758143786
permissions -rw-r--r--
Constant "If" is now local
     1 (*  Title:      HOL/Reconstruction.thy
     2     ID: $Id$
     3     Author:     Lawrence C Paulson
     4     Copyright   2004  University of Cambridge
     5 *)
     6 
     7 header{*Attributes for Reconstructing External Resolution Proofs*}
     8 
     9 theory Reconstruction
    10     imports Hilbert_Choice Map Infinite_Set Extraction
    11     uses "Tools/res_lib.ML"
    12 	  "Tools/res_clause.ML"
    13 	  "Tools/res_skolem_function.ML"
    14 	  "Tools/res_axioms.ML"
    15 	  "Tools/res_types_sorts.ML"
    16 
    17       "Tools/ATP/recon_prelim.ML"
    18  	  "Tools/ATP/recon_order_clauses.ML"
    19  	  "Tools/ATP/recon_translate_proof.ML"
    20  	  "Tools/ATP/recon_parse.ML"
    21  	  "Tools/ATP/recon_transfer_proof.ML"
    22 	  "Tools/ATP/VampCommunication.ML"
    23 	  "Tools/ATP/VampireCommunication.ML"
    24 	  "Tools/ATP/SpassCommunication.ML"
    25 	  "Tools/ATP/watcher.sig"
    26 	  "Tools/ATP/watcher.ML"
    27 	  "Tools/ATP/res_clasimpset.ML"
    28 	  "Tools/res_atp.ML"
    29 
    30       "Tools/reconstruction.ML"
    31 
    32 begin
    33 
    34 text{*Every theory of HOL must be a descendant or ancestor of this one!*}
    35 
    36 setup ResAxioms.clause_setup
    37 setup ResAxioms.meson_method_setup
    38 setup Reconstruction.setup
    39 
    40 end