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