src/HOL/ATP_Linkup.thy
changeset 21999 0cf192e489e2
parent 21977 7f7177a95189
child 23444 6d4703843f93
--- a/src/HOL/ATP_Linkup.thy	Thu Jan 04 17:52:28 2007 +0100
+++ b/src/HOL/ATP_Linkup.thy	Thu Jan 04 17:55:12 2007 +0100
@@ -11,11 +11,11 @@
 uses
   "Tools/polyhash.ML"
   "Tools/res_clause.ML"
-  "Tools/res_reconstruct.ML"
-  "Tools/ATP/watcher.ML"
   "Tools/ATP/reduce_axiomsN.ML"
   ("Tools/res_hol_clause.ML")
   ("Tools/res_axioms.ML")
+  ("Tools/res_reconstruct.ML")
+  ("Tools/ATP/watcher.ML")
   ("Tools/res_atp.ML")
   ("Tools/res_atp_provers.ML")
   ("Tools/res_atp_methods.ML")
@@ -83,8 +83,10 @@
 lemma iff_negative: "~P | ~Q | P=Q"
 by blast
 
-use "Tools/res_axioms.ML"
-use "Tools/res_hol_clause.ML"
+use "Tools/res_axioms.ML"      --{*requires the combinators declared above*}
+use "Tools/res_hol_clause.ML"  --{*requires the combinators*}
+use "Tools/res_reconstruct.ML"
+use "Tools/ATP/watcher.ML"
 use "Tools/res_atp.ML"
 
 setup ResAxioms.meson_method_setup