src/HOL/Reconstruction.thy
changeset 17846 6fd3261a1be0
parent 17819 1241e5d31d5b
child 18004 1883971957de
equal deleted inserted replaced
17845:1438291d57f0 17846:6fd3261a1be0
     8 
     8 
     9 theory Reconstruction
     9 theory Reconstruction
    10 imports Hilbert_Choice Map Infinite_Set Extraction
    10 imports Hilbert_Choice Map Infinite_Set Extraction
    11 uses "Tools/res_clause.ML"
    11 uses "Tools/res_clause.ML"
    12 	 "Tools/res_axioms.ML"
    12 	 "Tools/res_axioms.ML"
    13 	 "Tools/res_types_sorts.ML"
       
    14 	 "Tools/ATP/recon_order_clauses.ML"
    13 	 "Tools/ATP/recon_order_clauses.ML"
    15 	 "Tools/ATP/recon_translate_proof.ML"
    14 	 "Tools/ATP/recon_translate_proof.ML"
    16 	 "Tools/ATP/recon_parse.ML"
    15 	 "Tools/ATP/recon_parse.ML"
    17 	 "Tools/ATP/recon_transfer_proof.ML"
    16 	 "Tools/ATP/recon_transfer_proof.ML"
    18 	 "Tools/ATP/AtpCommunication.ML"
    17 	 "Tools/ATP/AtpCommunication.ML"