| Sat, 09 Dec 2006 18:05:38 +0100 | wenzelm | ML_Syntax.reserved(_names); | changeset | files |
| Sat, 09 Dec 2006 18:05:37 +0100 | wenzelm | TermSyntax.abbrev; | changeset | files |
| Sat, 09 Dec 2006 18:05:36 +0100 | wenzelm | added antiquotation abbrev; | changeset | files |
| Sat, 09 Dec 2006 18:05:34 +0100 | wenzelm | added print_abbrevs; | changeset | files |
| Fri, 08 Dec 2006 23:25:54 +0100 | wenzelm | tuned use_text; | changeset | files |
| Fri, 08 Dec 2006 23:25:53 +0100 | wenzelm | added 'help' command (same of 'print_commands'); | changeset | files |
| Fri, 08 Dec 2006 23:25:52 +0100 | wenzelm | more careful evaluation of ML text, prevents spurious output; | changeset | files |