src/HOLCF/FOCUS/ROOT.ML
author wenzelm
Thu, 14 Jul 2005 19:28:26 +0200
changeset 16844 60ab395e6da5
parent 15188 9d57263faf9e
child 24106 f2965bf954dc
permissions -rw-r--r--
with_path;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
     1
(*  Title:      HOLCF/FOCUS/ROOT.ML
11355
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";