<commit_before>(*  Title:      HOL/Reconstruction.thy
    ID:         $Id$
    Author:     <NAME>
    Copyright   2004  University of Cambridge
*)

header{* Reconstructing external resolution proofs *}

theory Reconstruction
imports Hilbert_Choice Map Infinite_Set Extraction
uses "Tools/res_clause.ML"
	 "Tools/res_axioms.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<commit_msg>Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses.<commit_after>(*  Title:      HOL/Reconstruction.thy
    ID:         $Id$
    Author:     <NAME>
    Copyright   2004  University of Cambridge
*)

header{* Reconstructing external resolution proofs *}

theory Reconstruction
imports Hilbert_Choice Map Infinite_Set Extraction
uses "Tools/res_clause.ML"
         "Tools/res_hol_clause.ML"
	 "Tools/res_axioms.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
{'fraction_non_alphanumeric': 0.1004566210045662, 'fraction_numerical': 0.005218525766470972, 'mean_word_length': 4.079470198675497, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '90833', 'n_tokens_mistral': 589, 'n_tokens_neox': 536, 'n_words': 101}