| Sat, 08 Apr 2006 22:51:31 +0200 | wenzelm | removed fix_mixfix; | changeset | files |
| Sat, 08 Apr 2006 22:51:30 +0200 | wenzelm | abbreviation(_i): do not expand abbreviations, do not use derived_def; | changeset | files |
| Sat, 08 Apr 2006 22:51:28 +0200 | wenzelm | add_abbrevs(_i): support print mode; | changeset | files |
| Sat, 08 Apr 2006 22:51:26 +0200 | wenzelm | abbrevs: support print mode; | changeset | files |
| Sat, 08 Apr 2006 22:51:25 +0200 | wenzelm | simplified handling of authentic syntax (cf. early externing in consts.ML); | changeset | files |
| Sat, 08 Apr 2006 22:51:23 +0200 | wenzelm | 'abbreviation': optional print mode; | changeset | files |
| Sat, 08 Apr 2006 22:51:22 +0200 | wenzelm | tuned; | changeset | files |