[isabelle-dev] token translations

Makarius makarius at sketis.net
Sat Jan 26 13:33:54 CET 2008


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




More information about the isabelle-dev mailing list