src/Pure/table.ML
Sun, 28 Dec 1997 14:55:34 +0100 wenzelm tuned;
Sat, 27 Dec 1997 21:49:45 +0100 wenzelm Generic tables (lacking delete operation). Implemented as 2-3 trees.
less more (0) tip