simultaneous use_thys;

--- a/src/HOL/AxClasses/ROOT.ML	Tue Jul 31 22:21:18 2007 +0200
+++ b/src/HOL/AxClasses/ROOT.ML	Tue Jul 31 22:21:20 2007 +0200
@@ -1,4 +1,3 @@
+(* $Id$ *)
 
-time_use_thy "Semigroups";
-time_use_thy "Group";
-time_use_thy "Product";
+use_thys ["Semigroups", "Group", "Product"];

--- a/src/HOL/Extraction/ROOT.ML	Tue Jul 31 22:21:18 2007 +0200
+++ b/src/HOL/Extraction/ROOT.ML	Tue Jul 31 22:21:20 2007 +0200
@@ -8,8 +8,5 @@
   warning "HOL proof terms required for running extraction examples"
 else
   (proofs := 2;
-   time_use_thy "QuotRem";
-   time_use_thy "Warshall";
-   time_use_thy "Higman";
    no_document time_use_thy "Efficient_Nat";
-   time_use_thy "Pigeonhole");
+   use_thys ["QuotRem", "Warshall", "Higman", "Pigeonhole"]);

--- a/src/HOL/Hoare/ROOT.ML	Tue Jul 31 22:21:18 2007 +0200
+++ b/src/HOL/Hoare/ROOT.ML	Tue Jul 31 22:21:20 2007 +0200
@@ -4,10 +4,5 @@
     Copyright   1998-2003 TUM
 *)
 
-time_use_thy "Examples";
-time_use_thy "ExamplesAbort";
-time_use_thy "Pointers0";
-time_use_thy "Pointer_Examples";
-time_use_thy "Pointer_ExamplesAbort";
-time_use_thy "SchorrWaite";
-time_use_thy "Separation";
+use_thys ["Examples", "ExamplesAbort", "Pointers0", "Pointer_Examples",
+  "Pointer_ExamplesAbort", "SchorrWaite", "Separation"];

--- a/src/HOL/HoareParallel/ROOT.ML	Tue Jul 31 22:21:18 2007 +0200
+++ b/src/HOL/HoareParallel/ROOT.ML	Tue Jul 31 22:21:20 2007 +0200
@@ -1,5 +1,3 @@
+(* $Id$ *)
 
-time_use_thy "OG_Examples";
-time_use_thy "Gar_Coll";
-time_use_thy "Mul_Gar_Coll";
-time_use_thy "RG_Examples";
+use_thys ["OG_Examples", "Gar_Coll", "Mul_Gar_Coll", "RG_Examples"];

--- a/src/HOL/IMP/ROOT.ML	Tue Jul 31 22:21:18 2007 +0200
+++ b/src/HOL/IMP/ROOT.ML	Tue Jul 31 22:21:20 2007 +0200
@@ -6,9 +6,4 @@
 Caveat: HOLCF/IMP depends on HOL/IMP
 *)
 
-time_use_thy "Expr";
-time_use_thy "Transition";
-time_use_thy "VC";
-time_use_thy "Examples";
-time_use_thy "Compiler0";
-time_use_thy "Compiler";
+use_thys ["Expr", "Transition", "VC", "Examples", "Compiler0", "Compiler"];

--- a/src/HOL/Induct/ROOT.ML	Tue Jul 31 22:21:18 2007 +0200
+++ b/src/HOL/Induct/ROOT.ML	Tue Jul 31 22:21:20 2007 +0200
@@ -1,16 +1,6 @@
 
 (* $Id$ *)
 
-time_use_thy "Mutil";
-time_use_thy "QuoDataType";
-time_use_thy "QuoNestedDataType";
-time_use_thy "Term";
-time_use_thy "ABexp";
-time_use_thy "Tree";
-time_use_thy "Ordinals";
-time_use_thy "Sigma_Algebra";
-time_use_thy "Comb";
-time_use_thy "PropLog";
-time_use_thy "SList";
-time_use_thy "LFilter";
-time_use_thy "Com";
+use_thys ["Mutil", "QuoDataType", "QuoNestedDataType", "Term",
+  "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog",
+  "SList", "LFilter", "Com"];

--- a/src/HOL/Lambda/ROOT.ML	Tue Jul 31 22:21:18 2007 +0200
+++ b/src/HOL/Lambda/ROOT.ML	Tue Jul 31 22:21:20 2007 +0200
@@ -7,9 +7,8 @@
 Syntax.ambiguity_level := 100;
 proofs := 2;
 
-use_thy "Eta";
 no_document use_thy "Accessible_Part";
-use_thy "StrongNorm";
+use_thys ["Eta", "StrongNorm"];
 if HOL_proofs < 2 then
   warning "HOL proof terms required for running theory WeakNorm"
 else use_thy "WeakNorm";

--- a/src/HOL/Library/Library/ROOT.ML	Tue Jul 31 22:21:18 2007 +0200
+++ b/src/HOL/Library/Library/ROOT.ML	Tue Jul 31 22:21:20 2007 +0200
@@ -1,6 +1,3 @@
 (* $Id$ *)
 
-use_thy "Library";
-use_thy "List_Prefix";
-use_thy "List_lexord";
-use_thy "SCT_Examples";
+use_thys ["Library", "List_Prefix", "List_lexord", "SCT_Examples"];

--- a/src/HOL/NumberTheory/ROOT.ML	Tue Jul 31 22:21:18 2007 +0200
+++ b/src/HOL/NumberTheory/ROOT.ML	Tue Jul 31 22:21:20 2007 +0200
@@ -1,12 +1,5 @@
 (* $Id$ *)
 
-no_document use_thy "Infinite_Set";
-no_document use_thy "Permutation";
-no_document use_thy "Primes";
-
-use_thy "Fib";
-use_thy "Factorization";
-use_thy "Chinese";
-use_thy "WilsonRuss";
-use_thy "WilsonBij";
-use_thy "Quadratic_Reciprocity";
+no_document use_thys ["Infinite_Set", "Permutation", "Primes"];
+use_thys ["Fib", "Factorization", "Chinese", "WilsonRuss",
+  "WilsonBij", "Quadratic_Reciprocity"];

--- a/src/HOL/Prolog/ROOT.ML	Tue Jul 31 22:21:18 2007 +0200
+++ b/src/HOL/Prolog/ROOT.ML	Tue Jul 31 22:21:20 2007 +0200
@@ -3,5 +3,4 @@
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
 *)
 
-use_thy"Test";
-use_thy"Type";
\ No newline at end of file
+use_thys ["Test", "Type"];

--- a/src/HOL/SET-Protocol/ROOT.ML	Tue Jul 31 22:21:18 2007 +0200
+++ b/src/HOL/SET-Protocol/ROOT.ML	Tue Jul 31 22:21:20 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/SET-Protocol/ROOT
+(*  Title:      HOL/SET-Protocol/ROOT.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2003  University of Cambridge
@@ -6,11 +6,5 @@
 Root file for the SET protocol proofs.
 *)
 
-goals_limit := 1;
-set timing;
-
 no_document use_thy "NatPair";
-time_use_thy "Cardholder_Registration";
-time_use_thy "Merchant_Registration";
-time_use_thy "Purchase";
-
+use_thys ["Cardholder_Registration", "Merchant_Registration", "Purchase"];