[isabelle-dev] Subscripts within identifiers

[Lars Noschinski]

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