src/Pure/General/README
changeset 6644 123b215882ae
parent 6634 6f74e7aa5b4d
child 9095 3b26cc949016
equal deleted inserted replaced
6643:ff827fccffb5 6644:123b215882ae
    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   Scan          (generic scanner toolbox)
       
    17   Source        (co-algebraic data sources)
       
    18   Symbol        (generalized characters)
    17   Path          (abstract algebra of file paths)
    19   Path          (abstract algebra of file paths)
       
    20   Url           (basic URL support)
    18   File          (file system operations)
    21   File          (file system operations)
    19   Buffer	(simple string buffers)
    22   Buffer	(simple string buffers)
    20   History       (histories of values, with undo and redo)
    23   History       (histories of values, with undo and redo)
    21   Source        (co-algebraic data sources)
       
    22   Symbol        (generalized characters)
       
    23   Pretty        (generic pretty printing module)
    24   Pretty        (generic pretty printing module)
    24   Use		(enhanced ML 'use' command)