[isabelle-dev] Subscripts within identifiers

Alexander Krauss krauss at in.tum.de
Sat Jul 13 22:42:42 CEST 2013


On 07/10/2013 07:25 PM, Makarius wrote:

> Even simpler would be to invent a name for some variant of \<omega> that
> is not considered a letter, and use that with \<^sup> as before.  That
> would be analogous to \<epsilon> vs. \<some>.

Does the mapping from Isabelle symbols to Unicode code points have to be 
injective? Otherwise, this would be an easy way to escape the problem: 
Just have \<omegasym>, which displays as omega, but is not a letter...

Alex






More information about the isabelle-dev mailing list