src/HOL/ex/ROOT.ML
changeset 14569 78b75a9eec01
parent 14494 48ae8d678d88
child 14592 dd1a2905ea73
--- a/src/HOL/ex/ROOT.ML	Thu Apr 15 13:04:50 2004 +0200
+++ b/src/HOL/ex/ROOT.ML	Thu Apr 15 14:17:45 2004 +0200
@@ -30,10 +30,15 @@
 time_use_thy "MergeSort";
 time_use_thy "Puzzle";
 
+no_document use_thy "List_Prefix";
+time_use_thy "Exceptions";
+
 time_use_thy "IntRing";
 
 time_use_thy "set";
 time_use_thy "MT";
+
+no_document use_thy "FuncSet";
 time_use_thy "Tarski";
 
 time_use_thy "SVC_Oracle";
@@ -41,4 +46,6 @@
 
 time_use_thy "Refute_Examples";
 
+no_document use_thy "Word";
 time_use_thy "Adder";
+