[isabelle-dev] token translations

Makarius 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"
> 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.


More information about the isabelle-dev mailing list