src/Pure/Syntax/token_trans.ML
Mon, 03 Mar 1997 14:14:04 +0100 wenzelm improved xterm, xterm_color;
less more (0) -1 tip