src/Pure/General/buffer.ML
2000-05-05 wenzelm 2000-05-05 GPLed;
1999-10-07 wenzelm 1999-10-07 removed write_nonempty;
1999-10-06 wenzelm 1999-10-06 added write_nonempty;
1999-03-09 wenzelm 1999-03-09 simple string buffers;