On 02.07.2013 18:00, Makarius wrote:
* There is just one \<^sub> and \<^sup> control symbol to that effect;
\<^isub> and \<^isup> remain within the infinite collection of
Isabelle symbols without any special meaning.
I.e., in the notation below they are not are LETTERs anymore and the
then-current IDEs will stop rendering them as sub-/superscripts?
I do not understand the LETTER aspect in this question. The front-ends
interpret certain control symbols independently of these token syntax
considerations: \<^sub>1 is rendered accordingly, wherever it occurs.
I meant to refer to "\<^isub>" and "\<^isup>" only in my question above.
As far as I inderstood your post, only LETTERs, DIGITs, "_" and a
restricted usage of "\<^sub>" may occur in identifiers. So the LETTER
aspect of my question boils down to whether these symbols are still
going to be allowed in identifiers.
("_ \<rightarrow>\<^isup>*\<index> _" [100,100] 40)
[...]
The above looks fine to me. It would merely come out as
\<rightarrow>\<^sup>*\<index>. The \<index> part then uses
\<^bsub>..\<^esub> as usual. (Many years ago there would have been a
conflict with \<^sub>DIGIT for the index slot, but that has disappeared
some years ago.)
Ok, then my theories shouldn't have any problems with the proposed changes.
-- Lars
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
