src/Pure/General/buffer.ML
Tue, 09 Mar 1999 12:08:50 +0100 wenzelm simple string buffers;
less more (0) tip