src/HOL/ex/ROOT.ML
changeset 15037 19b3b0382303
parent 14603 985eb6708207
child 15871 e524119dbf19
     1.1 --- a/src/HOL/ex/ROOT.ML	Sun Jul 11 20:35:50 2004 +0200
     1.2 +++ b/src/HOL/ex/ROOT.ML	Mon Jul 12 12:11:46 2004 +0200
     1.3 @@ -30,9 +30,6 @@
     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 "Lagrange";
    1.11  
    1.12  time_use_thy "set";