src/HOL/ex/ROOT.ML
changeset 3125 3f0ab2c306f7
parent 2987 becc227bad4d
child 3243 a42653373043
equal deleted inserted replaced
3124:1c0dfa7ebb72 3125:3f0ab2c306f7
    14 time_use     "meson.ML";
    14 time_use     "meson.ML";
    15 time_use     "mesontest.ML";
    15 time_use     "mesontest.ML";
    16 (** time_use "mesontest2.ML";  ULTRA SLOW **)
    16 (** time_use "mesontest2.ML";  ULTRA SLOW **)
    17 time_use_thy "String";
    17 time_use_thy "String";
    18 time_use_thy "BT";
    18 time_use_thy "BT";
    19 time_use_thy "Perm";
       
    20 time_use_thy "Comb";
       
    21 time_use_thy "InSort";
    19 time_use_thy "InSort";
    22 time_use_thy "Qsort";
    20 time_use_thy "Qsort";
    23 time_use_thy "LexProd";
    21 time_use_thy "LexProd";
    24 time_use_thy "Puzzle";
    22 time_use_thy "Puzzle";
    25 time_use_thy "Mutil";
       
    26 time_use_thy "Primes";
    23 time_use_thy "Primes";
    27 time_use_thy "NatSum";
    24 time_use_thy "NatSum";
    28 time_use     "set.ML";
    25 time_use     "set.ML";
    29 time_use_thy "SList";
       
    30 time_use_thy "LFilter";
       
    31 time_use_thy "Acc";
       
    32 time_use_thy "PropLog";
       
    33 time_use_thy "Term";
       
    34 time_use_thy "Simult";
       
    35 time_use_thy "MT";
    26 time_use_thy "MT";
    36 
    27 
    37 writeln "END: Root file for HOL examples";
    28 writeln "END: Root file for HOL examples";