On Sat, 26 Jan 2008, Steven Obua wrote: > I am using the Isar token translation mechanism to modify the latex > generation of Isabelle.
> But it does not work for the main output of a theory, like
>
> lemma "balabla"
> sorry
>
> The token translations are not applied to "balabla".
This is because token translations are only used when printing terms, not
when presenting theory sources.
Makarius
