# HG changeset patch # User quigley # Date 1112888751 -7200 # Node ID 28cc2314c7ff8cdd0f60a54ab655135d94057091 # Parent 8770edbf8f288adffb53ae5bcff06d0ad6eb8893 Reconstruction.thy and IsaMakefile updated diff -r 8770edbf8f28 -r 28cc2314c7ff src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Apr 07 14:07:40 2005 +0200 +++ b/src/HOL/IsaMakefile Thu Apr 07 17:45:51 2005 +0200 @@ -107,13 +107,13 @@ Tools/primrec_package.ML Tools/prop_logic.ML \ Tools/recdef_package.ML Tools/recfun_codegen.ML Tools/record_package.ML \ Tools/reconstruction.ML Tools/refute.ML Tools/refute_isar.ML \ - Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\ - Tools/res_axioms.ML Tools/res_types_sorts.ML \ Tools/rewrite_hol_proof.ML Tools/sat_solver.ML Tools/specification_package.ML \ Tools/split_rule.ML Tools/typedef_package.ML \ Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \ Wellfounded_Recursion.thy Wellfounded_Relations.thy arith_data.ML antisym_setup.ML \ blastdata.ML cladata.ML \ + 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_prelim.ML Tools/ATP/recon_gandalf_base.ML Tools/ATP/recon_order_clauses.ML\ Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.ML Tools/ATP/recon_reconstruct_proof.ML \ Tools/ATP/recon_transfer_proof.ML Tools/ATP/myres_axioms.ML Tools/ATP/res_clasimpset.ML \ diff -r 8770edbf8f28 -r 28cc2314c7ff src/HOL/Reconstruction.thy --- a/src/HOL/Reconstruction.thy Thu Apr 07 14:07:40 2005 +0200 +++ b/src/HOL/Reconstruction.thy Thu Apr 07 17:45:51 2005 +0200 @@ -14,6 +14,19 @@ "Tools/res_axioms.ML" "Tools/res_types_sorts.ML" + "Tools/ATP/recon_prelim.ML" + "Tools/ATP/recon_gandalf_base.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/VampireCommunication.ML" + "Tools/ATP/SpassCommunication.ML" + "Tools/ATP/modUnix.ML" + "Tools/ATP/watcher.sig" + "Tools/ATP/watcher.ML" + "Tools/res_atp.ML" + "Tools/reconstruction.ML" begin