[isabelle-dev] Subscripts within identifiers

Gerwin Klein Gerwin.Klein at nicta.com.au
Fri Aug 9 09:22:55 CEST 2013

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..



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.

More information about the isabelle-dev mailing list