src/Pure/General/buffer.ML
2009-01-02 ago removed unused add_substring;
2008-08-27 ago renamed Buffer.write to File.write_buffer;
2008-04-03 ago output: canonical argument order (as opposed to write);
2008-03-31 ago added add_substring;
2007-07-11 ago added markup operation;
2007-06-03 ago removed obsolete Library.seq;
2006-12-03 ago Add output function
2005-11-09 ago tuned comments;
2005-08-16 ago tuned Buffer.add;
2005-07-06 ago tuned write: use File.write_list;
2004-06-21 ago Merged in license change from Isabelle2004
2000-05-05 ago GPLed;
1999-10-07 ago removed write_nonempty;
1999-10-06 ago added write_nonempty;
1999-03-09 ago simple string buffers;