isabelle: src/HOLCF/ex/ROOT.ML@a744f9749885 (annotated)

244 929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	1	(* Title: HOLCF/ex/ROOT
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	2	ID: $Id$
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	3	Author: Tobias Nipkow
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	4	Copyright 1994 TU Muenchen
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	5
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	6	Executes all examples for HOLCF.
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	7	*)
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	8
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	9	HOLCF_build_completed; (Cause examples to fail if HOLCF did)
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	10
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	11	writeln"Root file for HOLCF examples";
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	12	proof_timing := true;
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	13	time_use_thy "ex/Coind";
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	14	time_use_thy "ex/Hoare";
929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	15	time_use_thy "ex/Loop";
297 5ef75ff3baeb Franz fragen nipkow parents: 244 diff changeset	16	time_use_thy "ex/Dagstuhl";
5ef75ff3baeb Franz fragen nipkow parents: 244 diff changeset	17
244 929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	18	maketest "END: Root file for HOLCF examples";

author	lcp
	Thu, 12 Jan 1995 03:00:58 +0100
changeset 850	a744f9749885
parent 297	5ef75ff3baeb
child 893	f81cb7520372
permissions	-rw-r--r--