Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
combining the relevance filter with res_atp
authorpaulson
Wed, 15 Aug 2007 15:06:58 +0200
changeset 24288 4016baca4973
parent 24287 c857dac06da6
child 24289 bfd59eb6e24e
combining the relevance filter with res_atp
src/HOL/ATP_Linkup.thy file | annotate | diff | comparison | revisions
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions 
--- 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		\
isabelle