[isabelle-dev] token translations

[Makarius]

On Sat, 26 Jan 2008, Steven Obua wrote:

> Makarius wrote:
> 
> >This is because token translations are only used when printing terms, not
> >when presenting theory sources.
> >
> Yes, I noticed that.
> 
> Is there any quick hack around it ?

No way.


        Makarius