--- a/src/HOL/MetisExamples/ROOT.ML Wed Dec 19 16:52:07 2007 +0100
+++ b/src/HOL/MetisExamples/ROOT.ML Wed Dec 19 16:52:26 2007 +0100
@@ -2,13 +2,8 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
-Testing the metis method
+Testing the metis method.
*)
-time_use_thy "set";
-time_use_thy "BigO";
-time_use_thy "Abstraction";
-time_use_thy "BT";
-time_use_thy "Message";
-time_use_thy "Tarski";
-time_use_thy "TransClosure";
+use_thys ["set", "BigO", "Abstraction", "BT", "Message", "Tarski", "TransClosure"];
+