src/HOL/ex/ROOT.ML
changeset 14569 78b75a9eec01
parent 14494 48ae8d678d88
child 14592 dd1a2905ea73
     1.1 --- a/src/HOL/ex/ROOT.ML	Thu Apr 15 13:04:50 2004 +0200
     1.2 +++ b/src/HOL/ex/ROOT.ML	Thu Apr 15 14:17:45 2004 +0200
     1.3 @@ -30,10 +30,15 @@
     1.4  time_use_thy "MergeSort";
     1.5  time_use_thy "Puzzle";
     1.6  
     1.7 +no_document use_thy "List_Prefix";
     1.8 +time_use_thy "Exceptions";
     1.9 +
    1.10  time_use_thy "IntRing";
    1.11  
    1.12  time_use_thy "set";
    1.13  time_use_thy "MT";
    1.14 +
    1.15 +no_document use_thy "FuncSet";
    1.16  time_use_thy "Tarski";
    1.17  
    1.18  time_use_thy "SVC_Oracle";
    1.19 @@ -41,4 +46,6 @@
    1.20  
    1.21  time_use_thy "Refute_Examples";
    1.22  
    1.23 +no_document use_thy "Word";
    1.24  time_use_thy "Adder";
    1.25 +