| 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 |
| Sat, 08 Apr 2006 22:51:20 +0200 | wenzelm | pretty_term': early vs. late externing (support authentic syntax); | changeset | files |
| Sat, 08 Apr 2006 22:51:19 +0200 | wenzelm | print_theory: print abbreviations nicely; | changeset | files |
| Sat, 08 Apr 2006 22:51:17 +0200 | wenzelm | added intern/extern/extern_early; | changeset | files |