src/Pure/Syntax/token_trans.ML
Mon, 03 Mar 1997 14:14:04 +0100 wenzelm improved xterm, xterm_color;
Sat, 01 Mar 1997 20:09:50 +0100 wenzelm added color styles;
Fri, 28 Feb 1997 16:42:06 +0100 wenzelm Token translations for xterm and LaTeX output.
less more (0) tip