[isabelle-dev] Subscripts within identifiers
Makarius
makarius at sketis.net
Fri Jul 12 19:41:38 CEST 2013
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
More information about the isabelle-dev
mailing list