Mon, 16 Dec 1996 10:04:45 +0100 | wenzelm | added needs_filtered_use; | changeset | files |
Mon, 16 Dec 1996 10:04:12 +0100 | wenzelm | added write_charnames'; | changeset | files |
Mon, 16 Dec 1996 10:03:30 +0100 | wenzelm | now uses SymbolInput.use; | changeset | files |
Mon, 16 Dec 1996 10:02:48 +0100 | wenzelm | symbol_input.ML: Defines 'use' command with symbol input filtering. | changeset | files |
Mon, 16 Dec 1996 10:02:17 +0100 | wenzelm | added symbol_input.ML; | changeset | files |
Mon, 16 Dec 1996 10:01:40 +0100 | wenzelm | fixed comment; | changeset | files |