| Tue, 17 Sep 2024 17:51:55 +0200 | wenzelm | more explicit context for syn_ext/mixfix operations, but it often degenerates to background theory; | changeset | files |
| Tue, 17 Sep 2024 17:05:37 +0200 | wenzelm | obsolete --- superseded by Local_Theory.syntax_cmd; | changeset | files |
| Tue, 17 Sep 2024 11:32:11 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 17 Sep 2024 11:14:25 +0200 | wenzelm | unused (see 39261908e12f); | changeset | files |