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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
