src/HOL/MetisExamples/ROOT.ML
changeset 33027 9cf389429f6d
parent 33026 8f35633c4922
child 33028 9aa8bfb1649d
--- a/src/HOL/MetisExamples/ROOT.ML	Tue Oct 20 19:37:09 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-(*  Title:      HOL/MetisExamples/ROOT.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-
-Testing the metis method.
-*)
-
-use_thys ["set", "BigO", "Abstraction", "BT", "Message", "Tarski", "TransClosure"];
-