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

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1351 diff changeset	1	(* Title: HOLCF/ex/ROOT
244 929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1351 diff changeset	3	Author: Tobias Nipkow
244 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;
297 5ef75ff3baeb Franz fragen nipkow parents: 244 diff changeset	13
1351 4a960c012383 removed make_chart; clasohm parents: 1306 diff changeset	14	time_use_thy "Hoare";
4a960c012383 removed make_chart; clasohm parents: 1306 diff changeset	15	time_use_thy "Loop";
4a960c012383 removed make_chart; clasohm parents: 1306 diff changeset	16	time_use_thy "Fix2";
4a960c012383 removed make_chart; clasohm parents: 1306 diff changeset	17	time_use "loeckx.ML";
1306 7c9c96e3621b added make_chart clasohm parents: 1274 diff changeset	18
2236 c7869a443b14 Uses Basis Library equivalent of cd paulson parents: 1461 diff changeset	19	OS.FileSys.chDir "..";
244 929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	20	maketest "END: Root file for HOLCF examples";

author	paulson
	Wed, 27 Nov 1996 10:34:28 +0100
changeset 2236	c7869a443b14
parent 1461	6bcb44e4d6e5
child 2570	24d7e8fb8261
permissions	-rw-r--r--