diff -r 000000000000 -r a5a9c433f639 src/CCL/ex/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/CCL/ex/ROOT.ML Thu Sep 16 12:20:38 1993 +0200 @@ -0,0 +1,17 @@ +(* Title: CCL/ex/ROOT + ID: $Id$ + Author: Martin Coen, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +Executes all examples for Classical Computational Logic +*) + +CCL_build_completed; (*Cause examples to fail if CCL did*) + +writeln"Root file for CCL examples"; +proof_timing := true; +time_use_thy "ex/nat"; +time_use_thy "ex/list"; +time_use_thy "ex/stream"; +time_use_thy "ex/flag"; +maketest"END: Root file for CCL examples";