simultaneous use_thys;

--- a/src/ZF/AC/ROOT.ML	Sun Jul 22 21:20:56 2007 +0200
+++ b/src/ZF/AC/ROOT.ML	Sun Jul 22 21:20:56 2007 +0200
@@ -1,25 +1,10 @@
-(*  Title:      ZF/AC/ROOT
+(*  Title:      ZF/AC/ROOT.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
-Executes the proofs of the AC-equivalences, due to Krzysztof Grabczewski
+Proofs of AC-equivalences, due to Krzysztof Grabczewski.
 *)
 
-time_use_thy "WO6_WO1";
-time_use_thy "WO1_WO7";
-
-time_use_thy "AC7_AC9";
-
-time_use_thy "WO1_AC";
-
-time_use_thy "AC15_WO6";
-
-time_use_thy "WO2_AC16";
-time_use_thy "AC16_WO4";
-
-time_use_thy "AC17_AC1";
-
-time_use_thy "AC18_AC19";
-
-time_use_thy "DC";
+use_thys ["WO6_WO1", "WO1_WO7", "AC7_AC9", "WO1_AC", "AC15_WO6",
+  "WO2_AC16", "AC16_WO4", "AC17_AC1", "AC18_AC19", "DC"];

--- a/src/ZF/Constructible/ROOT.ML	Sun Jul 22 21:20:56 2007 +0200
+++ b/src/ZF/Constructible/ROOT.ML	Sun Jul 22 21:20:56 2007 +0200
@@ -6,6 +6,4 @@
 Inner Models, Absoluteness and Consistency Proofs
 *)
 
-use_thy "DPow_absolute";
-use_thy "AC_in_L";
-use_thy "Rank_Separation";
+use_thys ["DPow_absolute", "AC_in_L", "Rank_Separation"];

--- a/src/ZF/Induct/ROOT.ML	Sun Jul 22 21:20:56 2007 +0200
+++ b/src/ZF/Induct/ROOT.ML	Sun Jul 22 21:20:56 2007 +0200
@@ -6,24 +6,26 @@
 Inductive definitions.
 *)
 
+use_thys [
 (** Datatypes **)
-time_use_thy "Datatypes";       (*sample datatypes*)
-time_use_thy "Binary_Trees";    (*binary trees*)
-time_use_thy "Term";            (*recursion over the list functor*)
-time_use_thy "Ntree";           (*variable-branching trees; function demo*)
-time_use_thy "Tree_Forest";     (*mutual recursion*)
-time_use_thy "Brouwer";         (*Infinite-branching trees*)
-time_use_thy "Mutil";           (*mutilated chess board*)
+  "Datatypes",       (*sample datatypes*)
+  "Binary_Trees",    (*binary trees*)
+  "Term",            (*recursion over the list functor*)
+  "Ntree",           (*variable-branching trees; function demo*)
+  "Tree_Forest",     (*mutual recursion*)
+  "Brouwer",         (*Infinite-branching trees*)
+  "Mutil",           (*mutilated chess board*)
 
 (*by Sidi Ehmety: Multisets.  A parent is FoldSet, the "fold" function for
 finite sets*)
-time_use_thy "Multiset";
-time_use_thy "Rmap";            (*mapping a relation over a list*)
-time_use_thy "PropLog";         (*completeness of propositional logic*)
+  "Multiset",
+  "Rmap",            (*mapping a relation over a list*)
+  "PropLog",         (*completeness of propositional logic*)
 
 (*two Coq examples by Christine Paulin-Mohring*)
-time_use_thy "ListN";
-time_use_thy "Acc";
+  "ListN",
+  "Acc",
 
-time_use_thy "Comb";            (*Combinatory Logic example*)
-time_use_thy "Primrec";         (*Primitive recursive functions*)
+  "Comb",            (*Combinatory Logic example*)
+  "Primrec"          (*Primitive recursive functions*)
+];

--- a/src/ZF/UNITY/ROOT.ML	Sun Jul 22 21:20:56 2007 +0200
+++ b/src/ZF/UNITY/ROOT.ML	Sun Jul 22 21:20:56 2007 +0200
@@ -1,21 +1,18 @@
-(*  Title:      ZF/UNITY/ROOT
+(*  Title:      ZF/UNITY/ROOT.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
-Root file for ZF/UNITY proofs.
+ZF/UNITY proofs.
 *)
 
-add_path "../Induct";  (*for Multisets*)
-
-(*Simple examples: no composition*)
-time_use_thy"Mutex";
+use_thys [
+  (*Simple examples: no composition*)
+  "Mutex",
 
-(*Basic meta-theory*)
-time_use_thy "Guar";
+  (*Basic meta-theory*)
+  "Guar",
 
-(* Prefix relation; the Allocator example *)
-time_use_thy "Distributor";
-time_use_thy "Merge";
-time_use_thy "ClientImpl";
-time_use_thy "AllocImpl";
+  (*Prefix relation; the Allocator example*)
+  "Distributor", "Merge", "ClientImpl", "AllocImpl"
+];

--- a/src/ZF/ex/ROOT.ML	Sun Jul 22 21:20:56 2007 +0200
+++ b/src/ZF/ex/ROOT.ML	Sun Jul 22 21:20:56 2007 +0200
@@ -3,18 +3,17 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Executes miscellaneous examples for Zermelo-Fraenkel Set Theory.
+Miscellaneous examples for Zermelo-Fraenkel Set Theory.
 *)
 
-time_use_thy "misc";
-time_use_thy "Ring";		(*abstract algebra*)
-time_use_thy "Commutation";     (*abstract Church-Rosser theory*)
-time_use_thy "Primes";          (*GCD theory*)
-time_use_thy "NatSum";          (*Summing integers, squares, cubes, etc.*)
-time_use_thy "Ramsey";          (*Simple form of Ramsey's theorem*)
-time_use_thy "Limit";           (*Inverse limit construction of domains*)
-time_use_thy "BinEx";		(*Binary integer arithmetic*)
-
-(** CoDatatypes **)
-time_use_thy "LList";
-time_use_thy "CoUnit";
+use_thys [
+  "misc",
+  "Ring",             (*abstract algebra*)
+  "Commutation",      (*abstract Church-Rosser theory*)
+  "Primes",           (*GCD theory*)
+  "NatSum",           (*Summing integers, squares, cubes, etc.*)
+  "Ramsey",           (*Simple form of Ramsey's theorem*)
+  "Limit",            (*Inverse limit construction of domains*)
+  "BinEx",            (*Binary integer arithmetic*)
+  "LList", "CoUnit"   (*CoDatatypes*)
+];