--- a/src/HOL/IsaMakefile Thu May 26 16:50:07 2005 +0200
+++ b/src/HOL/IsaMakefile Thu May 26 16:50:20 2005 +0200
@@ -92,7 +92,7 @@
ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy \
Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy Set.ML \
Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/SpassCommunication.ML \
- Tools/ATP/VampireCommunication.ML Tools/ATP/modUnix.ML \
+ Tools/ATP/VampireCommunication.ML \
Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_parse.ML \
Tools/ATP/recon_prelim.ML Tools/ATP/recon_transfer_proof.ML \
Tools/ATP/recon_translate_proof.ML Tools/ATP/res_clasimpset.ML \
--- a/src/HOL/Reconstruction.thy Thu May 26 16:50:07 2005 +0200
+++ b/src/HOL/Reconstruction.thy Thu May 26 16:50:20 2005 +0200
@@ -14,20 +14,19 @@
"Tools/res_axioms.ML"
"Tools/res_types_sorts.ML"
- "Tools/ATP/recon_prelim.ML"
+ "Tools/ATP/recon_prelim.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/ATP/res_clasimpset.ML"
"Tools/res_atp.ML"
- "Tools/reconstruction.ML"
+ "Tools/reconstruction.ML"
begin