src/HOL/Induct/ROOT.ML
changeset 10259 93ec82d535f2
parent 9951 5610c4acb48d
child 10566 7ed4f5a6c63f
equal deleted inserted replaced
10258:d549f2534e6d 10259:93ec82d535f2
     4 *)
     4 *)
     5 
     5 
     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 "Acc";
       
    10 time_use_thy "MultisetOrder";
       
    11 time_use_thy "PropLog";
     9 time_use_thy "PropLog";
    12 time_use_thy "SList";
    10 time_use_thy "SList";
    13 setmp quick_and_dirty false     (* FIXME tmp hack *)
    11 setmp quick_and_dirty false     (* FIXME tmp hack *)
    14 time_use_thy "LFilter";
    12 time_use_thy "LFilter";
    15 time_use_thy "Term";
    13 time_use_thy "Term";