--- a/src/HOL/NumberTheory/ROOT.ML Sun Oct 01 18:29:25 2006 +0200
+++ b/src/HOL/NumberTheory/ROOT.ML Sun Oct 01 18:29:26 2006 +0200
@@ -1,5 +1,6 @@
(* $Id$ *)
+no_document use_thy "Infinite_Set";
no_document use_thy "Permutation";
no_document use_thy "Primes";