src/HOLCF/FOCUS/ROOT.ML
author schirmer
Sun, 05 Jun 2005 13:49:51 +0200
changeset 16272 bcf05183df9e
parent 15188 9d57263faf9e
child 16844 60ab395e6da5
permissions -rw-r--r--
typo
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
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 15039
diff changeset
    12
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";