isabelle: src/HOLCF/FOCUS/ROOT.ML@ccd9cb15c062 (annotated)

11350 4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	1	(* Title: HOLCF/FOCUS/ROOT.ML
11355 778c369559d9 tuned wenzelm parents: 11350 diff changeset	2	ID: $Id$
11350 4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	3	Author: David von Oheimb, TU Muenchen
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	4
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	5	ROOT file for the FOCUS extension of HOLCF.
15039 450fcf885133 added README oheimb parents: 14981 diff changeset	6	See README.html for further information.
11350 4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	7	*)
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	8
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	9	val banner = "HOLCF/FOCUS";
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	10	writeln banner;
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	11
16844 60ab395e6da5 with_path; wenzelm parents: 15188 diff changeset	12	with_path "~~/src/HOLCF/ex" use_thy "Fstreams";
11350 4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	13	use_thy "FOCUS";
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: diff changeset	14	use_thy "Buffer_adm";

author	wenzelm
	Tue, 10 Jul 2007 23:29:43 +0200
changeset 23719	ccd9cb15c062
parent 16844	60ab395e6da5
child 24106	f2965bf954dc
permissions	-rw-r--r--