src/HOL/ex/ROOT.ML
changeset 23271 3f9ef4bf3f31
parent 23193 1f2d94b6a8ef
child 23302 919d5c1fe509
     1.1 --- a/src/HOL/ex/ROOT.ML	Tue Jun 05 22:46:57 2007 +0200
     1.2 +++ b/src/HOL/ex/ROOT.ML	Tue Jun 05 22:46:58 2007 +0200
     1.3 @@ -8,9 +8,17 @@
     1.4  no_document use_thy "GCD";
     1.5  
     1.6  no_document time_use_thy "Classpackage";
     1.7 -no_document time_use_thy "Eval_examples";
     1.8 -no_document time_use_thy "Random";
     1.9 -no_document time_use_thy "Codegenerator_Rat";
    1.10 +
    1.11 +no_document time_use_thy "Eval";
    1.12 +time_use_thy "Eval_Examples";
    1.13 +
    1.14 +no_document time_use_thy "State_Monad";
    1.15 +no_document time_use_thy "Pretty_Int";
    1.16 +time_use_thy "Random";
    1.17 +
    1.18 +no_document time_use_thy "ExecutableRat";
    1.19 +no_document time_use_thy "EfficientNat";
    1.20 +time_use_thy "Codegenerator_Rat";
    1.21  no_document time_use_thy "Codegenerator";
    1.22  
    1.23  time_use_thy "Higher_Order_Logic";
    1.24 @@ -49,6 +57,8 @@
    1.25  time_use_thy "Puzzle";
    1.26  
    1.27  time_use_thy "Lagrange";
    1.28 +time_use_thy "Groebner_Examples";
    1.29 +
    1.30  time_use_thy "Commutative_RingEx";
    1.31  time_use_thy "Commutative_Ring_Complete";
    1.32  time_use_thy "Reflection";