# Theory Reconstruction

Up to index of Isabelle/HOL

theory Reconstruction
imports Hilbert_Choice Map Infinite_Set Extraction
uses Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML Tools/res_axioms.ML Tools/res_types_sorts.ML Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.ML Tools/ATP/recon_transfer_proof.ML Tools/ATP/AtpCommunication.ML Tools/ATP/watcher.ML Tools/ATP/res_clasimpset.ML Tools/res_atp.ML Tools/reconstruction.ML
begin

    (*  Title:      HOL/Reconstruction.thy
        ID:         $Id: Reconstruction.thy,v 1.28 2005/09/23 14:05:10 webertj Exp $
        Author:     Lawrence C Paulson
        Copyright   2004  University of Cambridge
    *)

    header{* Reconstructing external resolution proofs *}

    theory Reconstruction
    imports Hilbert_Choice Map Infinite_Set Extraction
    uses "Tools/res_lib.ML"

      "Tools/res_clause.ML"
      "Tools/res_skolem_function.ML"
      "Tools/res_axioms.ML"
      "Tools/res_types_sorts.ML"

      "Tools/ATP/recon_order_clauses.ML"
      "Tools/ATP/recon_translate_proof.ML"
      "Tools/ATP/recon_parse.ML"
      "Tools/ATP/recon_transfer_proof.ML"
      "Tools/ATP/AtpCommunication.ML"
      "Tools/ATP/watcher.ML"
      "Tools/ATP/res_clasimpset.ML"
      "Tools/res_atp.ML"
      "Tools/reconstruction.ML"

    begin

    setup ResAxioms.meson_method_setup
    setup Reconstruction.setup

    end