src/Pure/General/README
changeset 6634 6f74e7aa5b4d
parent 6317 128e592f5489
child 6644 123b215882ae
equal deleted inserted replaced
6633:2ed30ebd7e31 6634:6f74e7aa5b4d
    11   Graph		(graphs indexed by strings)
    11   Graph		(graphs indexed by strings)
    12   Object        (generic objects of arbitrary type)
    12   Object        (generic objects of arbitrary type)
    13   Seq           (unbounded sequences)
    13   Seq           (unbounded sequences)
    14   NameSpace     (hierarchically structured name spaces)
    14   NameSpace     (hierarchically structured name spaces)
    15   Position      (input positions)
    15   Position      (input positions)
       
    16   Scan          (generic scanner toolbox)
    16   Path          (abstract algebra of file paths)
    17   Path          (abstract algebra of file paths)
    17   File          (file system operations)
    18   File          (file system operations)
    18   Buffer	(simple string buffers)
    19   Buffer	(simple string buffers)
    19   History       (histories of values, with undo and redo)
    20   History       (histories of values, with undo and redo)
    20   Scan          (generic scanner toolbox)
       
    21   Source        (co-algebraic data sources)
    21   Source        (co-algebraic data sources)
    22   Symbol        (generalized characters)
    22   Symbol        (generalized characters)
    23   Pretty        (generic pretty printing module)
    23   Pretty        (generic pretty printing module)
    24   Use		(enhanced ML 'use' command)
    24   Use		(enhanced ML 'use' command)