# HG changeset patch
# User wenzelm
# Date 1198079546 -3600
# Node ID 43a1f08c5a2957f24f2c4f84686b96787ae80a09
# Parent  a7341f8ddf89c3552ff43ea1dda0856d39634b32
simultaneous use_thys;

diff -r a7341f8ddf89 -r 43a1f08c5a29 src/HOL/MetisExamples/ROOT.ML
--- 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"];
+