--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Metis.thy	Wed Jun 20 22:07:52 2007 +0200
@@ -0,0 +1,16 @@
+(*  Title:      HOL/Metis.thy
+    ID:         $Id$
+*)
+
+header {* The Metis prover (version 2.0 from 2007) *}
+
+theory Metis
+imports Main
+uses
+  "~~/src/Tools/Metis/metis.ML"
+  "Tools/metis_tools.ML"
+begin
+
+setup MetisTools.setup
+
+end