src/HOL/ex/ROOT.ML
changeset 3294 4c73b6508f53
parent 3243 a42653373043
child 3337 c056d328aa0e
equal deleted inserted replaced
3293:c05f73cf3227 3294:4c73b6508f53
     8 
     8 
     9 HOL_build_completed;    (*Cause examples to fail if HOL did*)
     9 HOL_build_completed;    (*Cause examples to fail if HOL did*)
    10 
    10 
    11 writeln "Root file for HOL examples";
    11 writeln "Root file for HOL examples";
    12 proof_timing := true;
    12 proof_timing := true;
       
    13 
       
    14 (**Some examples of recursive function definitions: the TFL package**)
       
    15 time_use_thy "Fib";
       
    16 time_use_thy "Primes";
       
    17 
       
    18 time_use_thy "NatSum";
    13 time_use     "cla.ML";
    19 time_use     "cla.ML";
    14 time_use     "meson.ML";
    20 time_use     "meson.ML";
    15 time_use     "mesontest.ML";
    21 time_use     "mesontest.ML";
    16 (** time_use "mesontest2.ML";  ULTRA SLOW **)
    22 (** time_use "mesontest2.ML";  ULTRA SLOW **)
    17 time_use_thy "String";
    23 time_use_thy "String";
    18 time_use_thy "BT";
    24 time_use_thy "BT";
    19 time_use_thy "InSort";
    25 time_use_thy "InSort";
    20 time_use_thy "Qsort";
    26 time_use_thy "Qsort";
    21 time_use_thy "Puzzle";
    27 time_use_thy "Puzzle";
    22 time_use_thy "Primes";
    28 
    23 time_use_thy "NatSum";
       
    24 time_use     "set.ML";
    29 time_use     "set.ML";
    25 time_use_thy "MT";
    30 time_use_thy "MT";
    26 
    31 
    27 writeln "END: Root file for HOL examples";
    32 writeln "END: Root file for HOL examples";