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