# HG changeset patch
# User wenzelm
# Date 1186174240 -7200
# Node ID 1a4607b7ad24245b7ec8734c8fc9c4203c4dd3ca
# Parent  63cc746667a060b0af9c002655c7c812252d5391
simultaneous use_thys;

diff -r 63cc746667a0 -r 1a4607b7ad24 src/HOL/Algebra/ROOT.ML
--- a/src/HOL/Algebra/ROOT.ML	Fri Aug 03 22:35:40 2007 +0200
+++ b/src/HOL/Algebra/ROOT.ML	Fri Aug 03 22:50:40 2007 +0200
@@ -4,29 +4,28 @@
     Author: Clemens Ballarin, started 24 September 1999
 *)
 
-(*** New development, based on explicit structures ***)
-
 (* Preliminaries from set and number theory *)
-
-no_document use_thy "FuncSet";
-no_document use_thy "Primes";
-no_document use_thy "Binomial";
+no_document use_thys ["FuncSet", "Primes", "Binomial"];
 
 
-(* Groups *)
+(*** New development, based on explicit structures ***)
 
-use_thy "FiniteProduct";	(* Product operator for commutative groups *)
-use_thy "Sylow";		(* Sylow's theorem *)
-use_thy "Bij";			(* Automorphism Groups *)
+use_thys [
+  (* Groups *)
+  "FiniteProduct",      (* Product operator for commutative groups *)
+  "Sylow",              (* Sylow's theorem *)
+  "Bij",                (* Automorphism Groups *)
 
-(* Rings *)
-
-use_thy "UnivPoly";		(* Rings and polynomials *)
-use_thy "IntRing";		(* Ideals and residue classes *)
+  (* Rings *)
+  "UnivPoly",           (* Rings and polynomials *)
+  "IntRing"             (* Ideals and residue classes *)
+];
 
 
 (*** Old development, based on axiomatic type classes.
      Will be withdrawn in future. ***)
 
-with_path "abstract" (no_document time_use_thy) "Abstract";   (*The ring theory*)
-with_path "poly"     (no_document time_use_thy) "Polynomial"; (*The full theory*)
+no_document use_thys [
+  "abstract/Abstract",  (*The ring theory*)
+  "poly/Polynomial"     (*The full theory*)
+];
diff -r 63cc746667a0 -r 1a4607b7ad24 src/HOL/Nominal/Examples/ROOT.ML
--- a/src/HOL/Nominal/Examples/ROOT.ML	Fri Aug 03 22:35:40 2007 +0200
+++ b/src/HOL/Nominal/Examples/ROOT.ML	Fri Aug 03 22:50:40 2007 +0200
@@ -5,15 +5,17 @@
 Various examples involving nominal datatypes.
 *)
 
-use_thy "CR";
-use_thy "CR_Takahashi";
-use_thy "Class";
-use_thy "Compile";
-use_thy "Fsub";
-use_thy "Height";
-use_thy "Lambda_mu";
-use_thy "SN";
-use_thy "Weakening";
-use_thy "Crary";
-use_thy "SOS";
-use_thy "LocalWeakening";
+use_thys [
+  "CR",
+  "CR_Takahashi",
+  "Class",
+  "Compile",
+  "Fsub",
+  "Height",
+  "Lambda_mu",
+  "SN",
+  "Weakening",
+  "Crary",
+  "SOS",
+  "LocalWeakening"
+];