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