src/HOLCF/ex/ROOT.ML
changeset 3951 d52a49a7d8f3
parent 3154 6e20bf579edb
child 4449 df30e75f670f
equal deleted inserted replaced
3950:e9d5bcae8351 3951:d52a49a7d8f3
     9 HOLCF_build_completed;    (*Cause examples to fail if HOLCF did*)
     9 HOLCF_build_completed;    (*Cause examples to fail if HOLCF did*)
    10 
    10 
    11 writeln"Root file for HOLCF examples";
    11 writeln"Root file for HOLCF examples";
    12 proof_timing := true;
    12 proof_timing := true;
    13 
    13 
    14 time_use_thy "Classlib";
       
    15 time_use_thy "Dnat";
    14 time_use_thy "Dnat";
    16 time_use_thy "Dlist";
       
    17 time_use_thy "Stream";
    15 time_use_thy "Stream";
    18 time_use_thy "Dagstuhl";
    16 time_use_thy "Dagstuhl";
    19 time_use_thy "Focus_ex";
    17 time_use_thy "Focus_ex";
    20 time_use_thy "Fix2";
    18 time_use_thy "Fix2";
    21 time_use_thy "Hoare";
    19 time_use_thy "Hoare";