src/HOLCF/explicit_domains/ROOT.ML
changeset 2679 3eac428cdd1b
parent 2678 d5fe793293ac
child 2680 20fa49e610ca
     1.1 --- a/src/HOLCF/explicit_domains/ROOT.ML	Mon Feb 24 09:46:12 1997 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,20 +0,0 @@
     1.4 -(*
     1.5 -    ID:         $Id$
     1.6 -    Author:     Franz Regensburger
     1.7 -    Copyright   1995 Technische Universitaet Muenchen
     1.8 -
     1.9 -*)
    1.10 -
    1.11 -HOLCF_build_completed;    (*Cause examples to fail if HOLCF did*)
    1.12 -
    1.13 -writeln"Root file for HOLCF examples: explicit domain axiomatisation";
    1.14 -proof_timing := true;
    1.15 -
    1.16 -time_use_thy "Dnat";
    1.17 -time_use_thy "Dnat2";
    1.18 -time_use_thy "Stream";
    1.19 -time_use_thy "Stream2";
    1.20 -time_use_thy "Dlist";
    1.21 -
    1.22 -OS.FileSys.chDir "..";
    1.23 -maketest "END: Root file for HOLCF examples: explicit domain axiomatization";