[isabelle-dev] Subscripts within identifiers

[Makarius]

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:

   A\<^sup>\<omega>

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


 	Makarius