| Mon, 09 Mar 1998 16:09:56 +0100 | wenzelm | adapted to new scanners and baroque chars; | changeset | files |
| Mon, 09 Mar 1998 16:09:32 +0100 | wenzelm | tuned some names; | changeset | files |
| Mon, 09 Mar 1998 16:09:06 +0100 | wenzelm | adapted to baroque chars; | changeset | files |
| Mon, 09 Mar 1998 16:08:37 +0100 | wenzelm | added merge_alists; | changeset | files |
| Mon, 09 Mar 1998 16:08:06 +0100 | wenzelm | Syntax.indexname; | changeset | files |
| Mon, 09 Mar 1998 16:07:22 +0100 | wenzelm | tuned comment; | changeset | files |
| Mon, 09 Mar 1998 16:07:03 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 09 Mar 1998 16:06:46 +0100 | wenzelm | replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML; | changeset | files |
| Mon, 09 Mar 1998 16:05:34 +0100 | wenzelm | replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML; | changeset | files |
| Sat, 07 Mar 1998 16:29:29 +0100 | nipkow | Removed `addsplits [expand_if]' | changeset | files |
| Fri, 06 Mar 1998 18:25:28 +0100 | wenzelm | added clasimp.ML; | changeset | files |
| Fri, 06 Mar 1998 16:05:04 +0100 | nipkow | Removed superfluous `op' | changeset | files |