[isabelle-dev] token translations
makarius at sketis.net
Sat Jan 26 12:21:41 CET 2008
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"
> The token translations are not applied to "balabla".
This is because token translations are only used when printing terms, not
when presenting theory sources.
More information about the isabelle-dev