| Fri, 28 Feb 1997 16:42:06 +0100 | wenzelm | Token translations for xterm and LaTeX output. | changeset | files |
| Fri, 28 Feb 1997 16:41:49 +0100 | wenzelm | added _mk_ofclass(S); | changeset | files |
| Fri, 28 Feb 1997 16:41:04 +0100 | wenzelm | added strlen (includes metric information); | changeset | files |
| Fri, 28 Feb 1997 16:40:08 +0100 | wenzelm | added token_translation interface; | changeset | files |
| Fri, 28 Feb 1997 16:39:30 +0100 | wenzelm | added add_tokentrfuns; | changeset | files |
| Fri, 28 Feb 1997 16:38:55 +0100 | wenzelm | added Syntax/token_trans.ML; | changeset | files |
| Fri, 28 Feb 1997 16:36:49 +0100 | wenzelm | added token_trans.ML; | changeset | files |