src/HOL/ex/ROOT.ML
changeset 3404 91a91790899a
parent 3337 c056d328aa0e
child 4449 df30e75f670f
equal deleted inserted replaced
3403:6cc663f6d62e 3404:91a91790899a
    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 
    13 
    14 (**Some examples of recursive function definitions: the TFL package**)
    14 (**Some examples of recursive function definitions: the TFL package**)
       
    15 time_use_thy "Recdef";
    15 time_use_thy "Fib";
    16 time_use_thy "Fib";
    16 time_use_thy "Primes";
    17 time_use_thy "Primes";
    17 time_use_thy "Primrec";
    18 time_use_thy "Primrec";
    18 
    19 
    19 time_use_thy "NatSum";
    20 time_use_thy "NatSum";