src/Pure/General/buffer.ML
Wed, 09 Nov 2005 16:26:47 +0100 wenzelm tuned comments;
Tue, 16 Aug 2005 13:42:33 +0200 wenzelm tuned Buffer.add;
Wed, 06 Jul 2005 10:41:46 +0200 wenzelm tuned write: use File.write_list;
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Fri, 05 May 2000 22:02:46 +0200 wenzelm GPLed;
Thu, 07 Oct 1999 12:19:21 +0200 wenzelm removed write_nonempty;
Wed, 06 Oct 1999 18:11:37 +0200 wenzelm added write_nonempty;
Tue, 09 Mar 1999 12:08:50 +0100 wenzelm simple string buffers;
less more (0) tip