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

Isabelle/2077168aa8f7 already provides that, but \<^isub> and \<^isup> are 
still there as alternative copy.

The tool "isabelle update_sub_sup" is a user convenience, and will also 
help our own conversion. Current AFP (e.g. 908304753f7d) works both before 
and after applying update_sub_sup to everything.

I did not push the red button yet, since the resulting change will be 
quite voluminous, although structurally trivial (apart from special 
considerations for sources in src/Pure and some manuals).

For the release, I can imagine some legacy option (off by default) to 
allow both old and new forms in sources.


 	Makarius