[isabelle-dev] Subscripts within identifiers

[Gerwin Klein]

On 08/08/2013, at 9:18 PM, Makarius <makarius at sketis.net> wrote:

> Together with our \<^sub>\<omega> this reconfirms my initial impression that it is better to have the asymmetry of \<^sub> for identifiers vs. \<^sup> for notation.  As a consequence, \<twosuperior> also becomes obsolete; \<onesuperior> and \<threesuperior> were never used in practice, and the other superscripted 4..9 from unicode never assigned in our default symbol interpretation (they are missing in the IsabelleText font).
[..]
> So everything is ready to push the red button ...

I don't have a strong opinion either way, so I'm Ok with trying it out..

Cheers,
Gerwin


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.