src/HOL/NumberTheory/ROOT.ML

--- 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"];