author | wenzelm |
Wed, 20 Jun 2007 23:19:16 +0200 | |
changeset 23444 | 6d4703843f93 |
parent 23443 | fd8ffc8a5709 |
child 23445 | 6908c13215d1 |
--- 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