[isabelle-dev] Subscripts within identifiers

[Alexander Krauss]

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