src/HOLCF/FOCUS/ROOT.ML
author wenzelm
Thu, 07 Aug 2008 22:32:03 +0200
changeset 27786 4525c6f5d753
parent 24106 f2965bf954dc
child 32960 69916a850301
permissions -rw-r--r--
added read_token -- with optional YXML encoding of position; tuned parse operations: print position instead of echoing input (now encoded!); do not export obsolete read operation;
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
24106
f2965bf954dc simultaneous use_thys;
wenzelm
parents: 16844
diff changeset
     9
use_thys ["Fstreams", "FOCUS", "Buffer_adm"];