[isabelle-dev] Subscripts within identifiers

Makarius 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>


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 mailing list