[isabelle-dev] Subscripts within identifiers
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...
More information about the isabelle-dev