[isabelle-dev] token translations

[Makarius]

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