src/Pure/General/output.ML
Sat, 29 May 2004 14:54:10 +0200 wenzelm output channels;
less more (0) tip