From: Makarius <makarius@sketis.net>
In principle this could be done for anything is printed via document
antiquotations, going through the Isabelle syntax engine. You can then
modify the presentation of certain atomic entities via the internal
concept of token translations.
This won't affect regular theory sources, though. This is because the
document preparation system does not really understand the structure of
the formal entities that it is typesetting.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC