obsolete (cf. ATP_Linkup.thy);

--- a/src/HOL/Metis.thy	Wed Jun 20 23:19:17 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(*  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