[isabelle-dev] Subscripts within identifiers
makarius at sketis.net
Fri Jul 12 16:35:05 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 )*
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.
More information about the isabelle-dev