[isabelle-dev] Subscripts within identifiers

[Makarius]

On Fri, 5 Jul 2013, Tobias Nipkow wrote:

> Am 05/07/2013 14:08, schrieb Makarius:
>>
>>   x\<^sub>2
>>   x\<^sup>2
>>
>> When I seen "x subscripted 2" it is by default an identifier, but "x
>> superscripted 2" is x-squared.
>
> I think this is not a good example. If you write "x\<isup>2" now it is an
> identifier and if you write "x\<^sup>2" it is illegal. If you refer to
> "x\<twosuperior>", that is a hack (but you could still write it).

Yes, that is a correct observation, and some minor additional confusion 
that I did not intend to address here: ISO-Latin has special characters 
for some superscripted digits, and unicode completes that to 0..9 (but we 
are not using them right now).  So the overlap could be limited to 
\<^sup>LETTER, without \<^sup>DIGIT.

I will make another empirical test to see what happens -- but this always 
takes hours (sometimes days) to get past small surprises.


 	Makarius