Reconstruction.thy and IsaMakefile updated
authorquigley
Thu Apr 07 17:45:51 2005 +0200 (2005-04-07)
changeset 1567828cc2314c7ff
parent 15677 8770edbf8f28
child 15679 28eb0fe50533
Reconstruction.thy and IsaMakefile updated
src/HOL/IsaMakefile
src/HOL/Reconstruction.thy
     1.1 --- a/src/HOL/IsaMakefile	Thu Apr 07 14:07:40 2005 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Apr 07 17:45:51 2005 +0200
     1.3 @@ -107,13 +107,13 @@
     1.4    Tools/primrec_package.ML Tools/prop_logic.ML \
     1.5    Tools/recdef_package.ML Tools/recfun_codegen.ML Tools/record_package.ML \
     1.6    Tools/reconstruction.ML Tools/refute.ML Tools/refute_isar.ML \
     1.7 -  Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\
     1.8 -  Tools/res_axioms.ML Tools/res_types_sorts.ML \
     1.9    Tools/rewrite_hol_proof.ML Tools/sat_solver.ML Tools/specification_package.ML \
    1.10    Tools/split_rule.ML Tools/typedef_package.ML \
    1.11    Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
    1.12    Wellfounded_Recursion.thy Wellfounded_Relations.thy arith_data.ML antisym_setup.ML \
    1.13    blastdata.ML cladata.ML \
    1.14 +  Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\
    1.15 +  Tools/res_axioms.ML Tools/res_types_sorts.ML \
    1.16    Tools/ATP/recon_prelim.ML  Tools/ATP/recon_gandalf_base.ML  Tools/ATP/recon_order_clauses.ML\
    1.17    Tools/ATP/recon_translate_proof.ML   Tools/ATP/recon_parse.ML   Tools/ATP/recon_reconstruct_proof.ML \
    1.18    Tools/ATP/recon_transfer_proof.ML  Tools/ATP/myres_axioms.ML   Tools/ATP/res_clasimpset.ML \
     2.1 --- a/src/HOL/Reconstruction.thy	Thu Apr 07 14:07:40 2005 +0200
     2.2 +++ b/src/HOL/Reconstruction.thy	Thu Apr 07 17:45:51 2005 +0200
     2.3 @@ -14,6 +14,19 @@
     2.4  	  "Tools/res_axioms.ML"
     2.5  	  "Tools/res_types_sorts.ML"
     2.6  
     2.7 +          "Tools/ATP/recon_prelim.ML"
     2.8 +	  "Tools/ATP/recon_gandalf_base.ML"
     2.9 + 	  "Tools/ATP/recon_order_clauses.ML"
    2.10 + 	  "Tools/ATP/recon_translate_proof.ML"
    2.11 + 	  "Tools/ATP/recon_parse.ML"
    2.12 + 	  "Tools/ATP/recon_transfer_proof.ML"
    2.13 +	  "Tools/ATP/VampireCommunication.ML"
    2.14 +	  "Tools/ATP/SpassCommunication.ML"
    2.15 +	  "Tools/ATP/modUnix.ML"
    2.16 +	  "Tools/ATP/watcher.sig"
    2.17 +	  "Tools/ATP/watcher.ML"
    2.18 +	  "Tools/res_atp.ML"
    2.19 +
    2.20            "Tools/reconstruction.ML"
    2.21  
    2.22  begin