--- 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*)
+];
--- 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"
+];