src/Pure/General/README
author wenzelm
Wed, 03 Feb 1999 16:28:13 +0100
changeset 6179 e40b647fd6d0
parent 6135 cf917037cfd4
child 6317 128e592f5489
permissions -rw-r--r--
added Use;


                                Pure/General/


This directory contains general purpose modules, all of which are
exported.

  TableFun      (generic tables)
  Symtab        (tables indexed by strings)
  GraphFun	(generic directed graphs)
  Graph		(graphs indexed by strings)
  Object        (generic objects of arbitrary type)
  Seq           (unbounded sequences)
  NameSpace     (hierarchically structured name spaces)
  Position      (input positions)
  Path          (abstract algebra of file paths)
  File          (file system operations)
  History       (histories of values, with undo and redo)
  Scan          (generic scanner toolbox)
  Source        (co-algebraic data sources)
  Symbol        (generalized characters)
  Pretty        (generic pretty printing module)
  Use		(enhanced ML 'use' command)