# HG changeset patch
# User wenzelm
# Date 1182374357 -7200
# Node ID 1794387c79a2f99978a426fc154556d1854ad85f
# Parent  6908c13215d1e5a9469cc2557adb84e73d9657a6
obsolete (cf. ATP_Linkup.thy);

diff -r 6908c13215d1 -r 1794387c79a2 src/HOL/Metis.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