src/HOLCF/explicit_domains/ROOT.ML
author regensbu
Fri, 06 Oct 1995 17:25:24 +0100
changeset 1274 ea0668a1c0ba
child 1351 4a960c012383
permissions -rw-r--r--
added 8bit pragmas added directory ax_ops for sections axioms and ops added directory domain for sections domain and generated this is the type definition package of David Oheimb

(*
    ID:         $Id$
    Author: 	Franz Regensburger
    Copyright   1995 Technische Universitaet Muenchen

*)

HOLCF_build_completed;    (*Cause examples to fail if HOLCF did*)

writeln"Root file for HOLCF examples: explicit domain axiomatisation";
proof_timing := true;
time_use_thy "explicit_domains/Dnat";
time_use_thy "explicit_domains/Dnat2";
time_use_thy "explicit_domains/Stream";
time_use_thy "explicit_domains/Stream2";
time_use_thy "explicit_domains/Dlist";

time_use_thy "explicit_domains/Coind";
time_use_thy "explicit_domains/Dagstuhl";
time_use_thy "explicit_domains/Focus_ex";

maketest "END: Root file for HOLCF examples: explicit domain axiomatization";