isabelle: src/Pure/General/README@3b26cc949016 (annotated)

6116 8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	1
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	2	Pure/General/
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	3
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	4
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	5	This directory contains general purpose modules, all of which are
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	6	exported.
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	7
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	8	TableFun (generic tables)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	9	Symtab (tables indexed by strings)
6135 cf917037cfd4 GraphFun (generic directed graphs); wenzelm parents: 6116 diff changeset	10	GraphFun (generic directed graphs)
cf917037cfd4 GraphFun (generic directed graphs); wenzelm parents: 6116 diff changeset	11	Graph (graphs indexed by strings)
6116 8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	12	Object (generic objects of arbitrary type)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	13	Seq (unbounded sequences)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	14	NameSpace (hierarchically structured name spaces)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	15	Position (input positions)
6634 6f74e7aa5b4d moved scan.ML; wenzelm parents: 6317 diff changeset	16	Scan (generic scanner toolbox)
6644 123b215882ae tuned; wenzelm parents: 6634 diff changeset	17	Source (co-algebraic data sources)
123b215882ae tuned; wenzelm parents: 6634 diff changeset	18	Symbol (generalized characters)
6116 8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	19	Path (abstract algebra of file paths)
6644 123b215882ae tuned; wenzelm parents: 6634 diff changeset	20	Url (basic URL support)
6116 8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	21	File (file system operations)
6317 128e592f5489 added Buffer; wenzelm parents: 6179 diff changeset	22	Buffer (simple string buffers)
6116 8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	23	History (histories of values, with undo and redo)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	24	Pretty (generic pretty printing module)
9095 3b26cc949016 new module for heaps paulson parents: 6644 diff changeset	25
3b26cc949016 new module for heaps paulson parents: 6644 diff changeset	26	Functor LeftistHeap implements heaps, which are used for best-first search.
3b26cc949016 new module for heaps paulson parents: 6644 diff changeset	27	It must be instantiated with a linearly ordered type.

author	paulson
	Tue, 20 Jun 2000 11:54:22 +0200
changeset 9095	3b26cc949016
parent 6644	123b215882ae
child 9119	8ca79837b41b
permissions	-rw-r--r--