--- a/src/HOL/ATP_Linkup.thy Wed Aug 15 13:50:47 2007 +0200
+++ b/src/HOL/ATP_Linkup.thy Wed Aug 15 15:06:58 2007 +0200
@@ -11,7 +11,6 @@
uses
"Tools/polyhash.ML"
"Tools/res_clause.ML"
- "Tools/ATP/reduce_axiomsN.ML"
("Tools/res_hol_clause.ML")
("Tools/res_axioms.ML")
("Tools/res_reconstruct.ML")
--- a/src/HOL/IsaMakefile Wed Aug 15 13:50:47 2007 +0200
+++ b/src/HOL/IsaMakefile Wed Aug 15 15:06:58 2007 +0200
@@ -96,7 +96,7 @@
Predicate.thy Product_Type.thy ROOT.ML Recdef.thy \
Record.thy Refute.thy Relation.thy Relation_Power.thy \
Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy Sum_Type.thy \
- Groebner_Basis.thy Tools/ATP/reduce_axiomsN.ML Tools/watcher.ML \
+ Groebner_Basis.thy Tools/watcher.ML \
Tools/Groebner_Basis/groebner.ML Tools/Groebner_Basis/misc.ML \
Tools/Groebner_Basis/normalizer.ML \
Tools/Groebner_Basis/normalizer_data.ML Tools/Qelim/cooper.ML \