isabelle: src/CCL/ex/ROOT.ML@4a10bc05210a (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;
121 d392174734e9 changed use_thy's parameter to exact theory name clasohm parents: 0 diff changeset	13	time_use_thy "ex/Nat";
d392174734e9 changed use_thy's parameter to exact theory name clasohm parents: 0 diff changeset	14	time_use_thy "ex/List";
d392174734e9 changed use_thy's parameter to exact theory name clasohm parents: 0 diff changeset	15	time_use_thy "ex/Stream";
d392174734e9 changed use_thy's parameter to exact theory name clasohm parents: 0 diff changeset	16	time_use_thy "ex/Flag";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	17	maketest"END: Root file for CCL examples";

author	nipkow
	Wed, 05 Jan 1994 19:43:46 +0100
changeset 216	4a10bc05210a
parent 121	d392174734e9
child 1000	0ad2b1da57ff
permissions	-rw-r--r--