# HG changeset patch
# User wenzelm
# Date 1182374356 -7200
# Node ID 6d4703843f93555c81e4e2d07795435b0137683a
# Parent  fd8ffc8a5709e46e6800c27acc2bb8f32fb34aa3
added Metis setup (from Metis.thy);

diff -r fd8ffc8a5709 -r 6d4703843f93 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