# HG changeset patch
# User paulson
# Date 1187183218 -7200
# Node ID 4016baca4973a03b99f205212b53f48fdb349d82
# Parent  c857dac06da6864b3c84a256af898b8946d79afe
combining the relevance filter with res_atp

diff -r c857dac06da6 -r 4016baca4973 src/HOL/ATP_Linkup.thy
--- 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")
diff -r c857dac06da6 -r 4016baca4973 src/HOL/IsaMakefile
--- 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		\