[isabelle-dev] Subscripts within identifiers

[Makarius]

On Wed, 10 Jul 2013, Makarius wrote:

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

Maybe Tjark wants to comment on that -- AFP/Kleene_Algebra is the main 
realistic application of that notation in the visible universe.

How would "Omega Algebras" fare with notation A\<^sup>\<infinity> instead 
of A\<^sup>\<omega>?


 	Makarius