src/HOLCF/ex/ROOT.ML
author oheimb
Fri Jan 31 16:56:32 1997 +0100 (1997-01-31)
changeset 2570 24d7e8fb8261
parent 2236 c7869a443b14
child 3154 6e20bf579edb
permissions -rw-r--r--
added Classlib.* and Witness.*,
moved (and updated) Coind.*, Dagstuhl.*, Dlist.*, Dnat.*, Focus_ex.*
and Stream.* from HOLCF/explicit_domains to here
adapted several proofs; now they work again.
Hope that the following strange errors (when committing) do not matter:
rlog error: RCS/Classlib.ML,v: No such file or directory
rlog error: RCS/Classlib.thy,v: No such file or directory
rlog error: RCS/Coind.ML,v: No such file or directory
rlog error: RCS/Coind.thy,v: No such file or directory
rlog error: RCS/Dagstuhl.ML,v: No such file or directory
rlog error: RCS/Dagstuhl.thy,v: No such file or directory
rlog error: RCS/Dlist.ML,v: No such file or directory
rlog error: RCS/Dlist.thy,v: No such file or directory
rlog error: RCS/Dnat.ML,v: No such file or directory
rlog error: RCS/Dnat.thy,v: No such file or directory
rlog error: RCS/Focus_ex.ML,v: No such file or directory
rlog error: RCS/Focus_ex.thy,v: No such file or directory
rlog error: RCS/Stream.ML,v: No such file or directory
rlog error: RCS/Stream.thy,v: No such file or directory
rlog error: RCS/Witness.ML,v: No such file or directory
rlog error: RCS/Witness.thy,v: No such file or directory
     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 "Classlib";
    15 time_use_thy "Witness";
    16 time_use_thy "Dnat";
    17 time_use_thy "Dlist";
    18 time_use_thy "Stream";
    19 time_use_thy "Dagstuhl";
    20 time_use_thy "Focus_ex";
    21 time_use_thy "Fix2";
    22 time_use_thy "Hoare";
    23 time_use_thy "Loop";
    24 time_use "loeckx.ML";
    25 
    26 OS.FileSys.chDir "..";
    27 maketest     "END: Root file for HOLCF examples";