added Metis setup (from Metis.thy);
authorwenzelm
Wed, 20 Jun 2007 23:19:16 +0200
changeset 23444 6d4703843f93
parent 23443 fd8ffc8a5709
child 23445 6908c13215d1
added Metis setup (from Metis.thy);
src/HOL/ATP_Linkup.thy
--- 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