src/Pure/Syntax/parser.ML
Mon, 04 Oct 1993 15:30:49 +0100 wenzelm lots of internal cleaning and tuning;
less more (0) tip