1.1 --- a/src/HOL/ex/ROOT.ML	Sun Oct 01 18:29:30 2006 +0200
     1.2 +++ b/src/HOL/ex/ROOT.ML	Sun Oct 01 18:29:31 2006 +0200
     1.3 @@ -20,12 +20,12 @@
     1.4  time_use_thy "Locales";
     1.5  time_use_thy "Records";
     1.6  time_use_thy "MonoidGroup";
     1.7 -time_use_thy "StringEx";
     1.8  time_use_thy "BinEx";
     1.9  setmp proofs 2 time_use_thy "Hilbert_Classical";
    1.10  time_use_thy "Antiquote";
    1.11  time_use_thy "Multiquote";
    1.12  
    1.13 +time_use_thy "PER";
    1.14  time_use_thy "NatSum";
    1.15  time_use_thy "ThreeDivides";
    1.16  time_use_thy "Intuitionistic";