isabelle: src/Pure/General/README@75a399c2781f (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)
9412 55e8230f5665 tuned HeapFun; wenzelm parents: 9119 diff changeset	12	HeapFun (heaps over linearly ordered types)
6116 8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	13	Object (generic objects of arbitrary type)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	14	Seq (unbounded sequences)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	15	NameSpace (hierarchically structured name spaces)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	16	Position (input positions)
6634 6f74e7aa5b4d moved scan.ML; wenzelm parents: 6317 diff changeset	17	Scan (generic scanner toolbox)
6644 123b215882ae tuned; wenzelm parents: 6634 diff changeset	18	Source (co-algebraic data sources)
123b215882ae tuned; wenzelm parents: 6634 diff changeset	19	Symbol (generalized characters)
6116 8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	20	Path (abstract algebra of file paths)
6644 123b215882ae tuned; wenzelm parents: 6634 diff changeset	21	Url (basic URL support)
6116 8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	22	File (file system operations)
6317 128e592f5489 added Buffer; wenzelm parents: 6179 diff changeset	23	Buffer (simple string buffers)
6116 8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; wenzelm parents: diff changeset	24	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	25	Pretty (generic pretty printing module)

author	berghofe
	Sat, 10 May 2003 20:53:02 +0200
changeset 13998	75a399c2781f
parent 9412	55e8230f5665
permissions	-rw-r--r--