> So here is a reform that works with minimal impact on existing sources: > > * Block sub/superscripts (\<^bsub>..\<^esub> and \<^bsup>..\<^esup>) > are not affected at all -- this is a different concept. > > * There is just one \<^sub> and \<^sup> control symbol to that effect; > \<^isub> and \<^isup> remain within the infinite collection of > Isabelle symbols without any special meaning. > > * \<^sub> and \<^sup> are no longer "letters". > > * Superscript is for explicit notation, e.g. "x\<^sup>2" for some > operator "_\<^sup>2" applied to term x. > > * Subscript may get used within identifiers, e.g. "x\<^sub>2" for a > variable of that name. > > The traditional ML identifier syntax is like this: > > LETTER = A .. Z a .. Z > DIGIT = 0 .. 9 > LETDIG = LETTER | DIGIT | _ | ' > > IDENTIFIER = LETTER LETDIG* > > So it is a strict letter followed by a sequence of liberal letters. > > Instead of making \<^sub> a "letter" as was done in Isabelle2003, the syntax > is changed like this: > > LETTER = A .. Z a .. Z \<alpha> ... \<A> ... \<a> ... etc. > DIGIT = 0 .. 9 > LETDIG = LETTER | DIGIT | _ | ' > SUBSCRIPT = \<^sub> > > IDENTIFIER = LETTER ( SUBSCRIPT? LETDIG )*
Pairing up subscript and letdig is definitely a good idea. One minor point: I think we should allow > IDENTIFIER = (SUBSCRIPT LETDIG)? LETTER ( SUBSCRIPT? LETDIG )* i.e. allow a subscript at the beginning of an identifier. This is probably not used much (or at all) currently, but I've seen this plenty of times in maths texts. Or is there a good reason against it? I'm less sure about the distinction between sub and sup. I can see it mostly aligns with current usage patterns, but I find this distinction even more confusing. Maybe that's just me and it's worth it if we can eliminate the isub/sub dimension. I can live with either, so I'll leave it to others to argue about it. 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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
