| Fri, 21 Dec 2001 23:18:27 +0100 | wenzelm | hide base name of "make", "fields", "extend", "truncate", "more", | changeset | files |
| Fri, 21 Dec 2001 23:17:35 +0100 | wenzelm | Theory.hide_space_i true; | changeset | files |
| Fri, 21 Dec 2001 23:17:12 +0100 | wenzelm | hide: flag for full/base name; | changeset | files |