src/HOL/ATP_Linkup.thy
changeset 23444 6d4703843f93
parent 21999 0cf192e489e2
child 23519 a4ffa756d8eb
--- a/src/HOL/ATP_Linkup.thy	Wed Jun 20 23:15:25 2007 +0200
+++ b/src/HOL/ATP_Linkup.thy	Wed Jun 20 23:19:16 2007 +0200
@@ -19,6 +19,8 @@
   ("Tools/res_atp.ML")
   ("Tools/res_atp_provers.ML")
   ("Tools/res_atp_methods.ML")
+  "~~/src/Tools/Metis/metis.ML"
+  ("Tools/metis_tools.ML")
 begin
 
 constdefs
@@ -103,4 +105,10 @@
 use "Tools/res_atp_methods.ML"
 setup ResAtpMethods.ResAtps_setup
 
+
+subsection {* The Metis prover *}
+
+use "Tools/metis_tools.ML"
+setup MetisTools.setup
+
 end