isabelle: src/CCL/ex/ROOT.ML@a5a9c433f639 (annotated)

0 a5a9c433f639 Initial revision clasohm parents: diff changeset	1	(* Title: CCL/ex/ROOT
a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
a5a9c433f639 Initial revision clasohm parents: diff changeset	3	Author: Martin Coen, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1993 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5
a5a9c433f639 Initial revision clasohm parents: diff changeset	6	Executes all examples for Classical Computational Logic
a5a9c433f639 Initial revision clasohm parents: diff changeset	7	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	8
a5a9c433f639 Initial revision clasohm parents: diff changeset	9	CCL_build_completed; (Cause examples to fail if CCL did)
a5a9c433f639 Initial revision clasohm parents: diff changeset	10
a5a9c433f639 Initial revision clasohm parents: diff changeset	11	writeln"Root file for CCL examples";
a5a9c433f639 Initial revision clasohm parents: diff changeset	12	proof_timing := true;
a5a9c433f639 Initial revision clasohm parents: diff changeset	13	time_use_thy "ex/nat";
a5a9c433f639 Initial revision clasohm parents: diff changeset	14	time_use_thy "ex/list";
a5a9c433f639 Initial revision clasohm parents: diff changeset	15	time_use_thy "ex/stream";
a5a9c433f639 Initial revision clasohm parents: diff changeset	16	time_use_thy "ex/flag";
a5a9c433f639 Initial revision clasohm parents: diff changeset	17	maketest"END: Root file for CCL examples";

author	clasohm
	Thu, 16 Sep 1993 12:20:38 +0200
changeset 0	a5a9c433f639
child 121	d392174734e9
permissions	-rw-r--r--