[isabelle-dev] Subscripts within identifiers
makarius at sketis.net
Wed Jul 10 16:54:17 CEST 2013
This is an update of this important thread.
It turned out that the symmetric version where both \<^sub> and \<^sup>
are allowed in the liberal part of identifiers works, with minimal impact
on applications of the known universe.
So the reformed identifier syntax is like this:
LETTER = A .. Z a .. Z \<alpha> ... \<A> ... \<a> ... etc.
DIGIT = 0 .. 9
LETDIG = LETTER | DIGIT | _ | '
CONTROL = \<^sub> | \<^sup>
IDENTIFIER = LETTER ( CONTROL? LETDIG )*
In preparation for the move, I have already pushed some homeopathic
changes to AFP, see aaec3f5a1ba6 and before. (Where is a sane AFP
repository browser on the Web?)
These changes are most just obscure details of relatively old-fashioned
AFP entries, such as Lazy-Lists-II. The main impact of practical relevance
is the following in Kleen_Algebra, which uses notation like this:
That is an instance of \<^sup>LETTER, i.e. the remaining overlap from the
earlier discussion on this thread. I have presently escaped the situation
by using \<^bsup> \<^esup> which looks almost the same in Latex, but is a
bit awkward in Isabelle/jEdit.
Unlike superscripted digits, I did not find an alternative unicode symbol
so far. One could recommend users using \<^sup>\<infinity> in such
More information about the isabelle-dev