src/HOL/Induct/ROOT.ML
changeset 10566 7ed4f5a6c63f
parent 10259 93ec82d535f2
child 10876 e12892e4666a
equal deleted inserted replaced
10565:7f7c1c3511e2 10566:7ed4f5a6c63f
     6 time_use_thy "Perm";
     6 time_use_thy "Perm";
     7 time_use_thy "Comb";
     7 time_use_thy "Comb";
     8 time_use_thy "Mutil";
     8 time_use_thy "Mutil";
     9 time_use_thy "PropLog";
     9 time_use_thy "PropLog";
    10 time_use_thy "SList";
    10 time_use_thy "SList";
    11 setmp quick_and_dirty false     (* FIXME tmp hack *)
       
    12 time_use_thy "LFilter";
    11 time_use_thy "LFilter";
    13 time_use_thy "Term";
    12 time_use_thy "Term";
    14 time_use_thy "ABexp";
    13 time_use_thy "ABexp";
    15 time_use_thy "Exp";
    14 time_use_thy "Exp";
    16 time_use_thy "Tree";
    15 time_use_thy "Tree";