src/Pure/General/buffer.ML
2007-07-11 wenzelm 2007-07-11 added markup operation;
2007-06-03 wenzelm 2007-06-03 removed obsolete Library.seq;
2006-12-03 aspinall 2006-12-03 Add output function
2005-11-09 wenzelm 2005-11-09 tuned comments;
2005-08-16 wenzelm 2005-08-16 tuned Buffer.add;
2005-07-06 wenzelm 2005-07-06 tuned write: use File.write_list;
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
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;