| changeset 6118 | caa439435666 |
| parent 5681 | 464913c6086a |
| child 7061 | 69d42b56151f |
| 6117:f9aad8ccd590 | 6118:caa439435666 |
|---|---|
1 (* Title: Pure/table.ML |
1 (* Title: Pure/General/table.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 |
4 |
5 Generic tables and tables indexed by strings. No delete operation. |
5 Generic tables and tables indexed by strings. No delete operation. |
6 Implemented as balanced 2-3 trees. |
6 Implemented as balanced 2-3 trees. |