src/HOLCF/ex/ROOT.ML
author wenzelm
Mon Oct 20 12:45:51 1997 +0200 (1997-10-20)
changeset 3951 d52a49a7d8f3
parent 3154 6e20bf579edb
child 4449 df30e75f670f
permissions -rw-r--r--
removed Dlist;
     1 (*  Title:      HOLCF/ex/ROOT
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1994 TU Muenchen
     5 
     6 Executes all examples for HOLCF. 
     7 *)
     8 
     9 HOLCF_build_completed;    (*Cause examples to fail if HOLCF did*)
    10 
    11 writeln"Root file for HOLCF examples";
    12 proof_timing := true;
    13 
    14 time_use_thy "Dnat";
    15 time_use_thy "Stream";
    16 time_use_thy "Dagstuhl";
    17 time_use_thy "Focus_ex";
    18 time_use_thy "Fix2";
    19 time_use_thy "Hoare";
    20 time_use_thy "Loop";
    21 time_use "loeckx.ML";
    22 
    23 OS.FileSys.chDir "..";
    24 maketest     "END: Root file for HOLCF examples";