isabelle: src/HOLCF/ex/ROOT.ML@599d3414b51d (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
6349 f7750d816c21 removed foo_build_completed -- now handled by session management (via usedir); wenzelm parents: 4449 diff changeset	9	writeln"Root file for HOLCF examples";
244 929fc2c63bd0 HOLCF examples nipkow parents: diff changeset	10
4449 df30e75f670f tuned; wenzelm parents: 3951 diff changeset	11	set proof_timing;
2570 24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: 2236 diff changeset	12	time_use_thy "Dnat";
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: 2236 diff changeset	13	time_use_thy "Stream";
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: 2236 diff changeset	14	time_use_thy "Dagstuhl";
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: 2236 diff changeset	15	time_use_thy "Focus_ex";
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: 2236 diff changeset	16	time_use_thy "Fix2";
1351 4a960c012383 removed make_chart; clasohm parents: 1306 diff changeset	17	time_use_thy "Hoare";
4a960c012383 removed make_chart; clasohm parents: 1306 diff changeset	18	time_use_thy "Loop";
4a960c012383 removed make_chart; clasohm parents: 1306 diff changeset	19	time_use "loeckx.ML";

author	wenzelm
	Fri, 10 Sep 1999 17:28:51 +0200
changeset 7535	599d3414b51d
parent 6349	f7750d816c21
child 9000	c20d58286a51
permissions	-rw-r--r--