src/Pure/Syntax/source.ML
Tue, 19 May 1998 17:16:18 +0200 wenzelm prompt made part of source;
less more (0) tip