[isabelle-dev] Subscripts within identifiers
makarius at sketis.net
Fri Jul 5 14:08:37 CEST 2013
On Tue, 2 Jul 2013, Gerwin Klein wrote:
> I'm less sure about the distinction between sub and sup. I can see it
> mostly aligns with current usage patterns, but I find this distinction
> even more confusing.
There are two aspects here: (1) common understanding of users and (2)
technical side-conditions. For me, both are speaking for that distinction:
sub for identifiers, sup for notation. E.g. consider the example again:
When I seen "x subscripted 2" it is by default an identifier, but "x
superscripted 2" is x-squared.
And technically, treating both the same would make most of our syntax
break down. You would have to put a space for x-squared: "x \<^sup>2".
> Maybe that's just me and it's worth it if we can eliminate the isub/sub
> dimension. I can live with either, so I'll leave it to others to argue
> about it.
This is how things came along in 2003:
date: Wed Oct 15 07:03:43 2003 +0200
files: NEWS lib/texinputs/isabelle.sty src/Pure/General/symbol.ML
use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid
conflict with locale subscript syntax)
So the seperate pair of control symbols (motivated by avoid the clash) had
the secondary effect of allowing \<^isub> within identifiers as well.
Maybe you remember more details yourself from back then. There are more
changesets involved for the whole story, though.
Just empirically, the \<^isup> notation hardly ever showed up in practice
in the last 10 years. The reason for that might be as lame as lack of
keyboard shortcuts in certain versions of Proof General, IIRC.
BTW, Isabelle/jEdit has quite nice keyboard and GUI tool support for
sub/superscripts, but just one set of them, not two. Visial rendering is
also better than in any Emacs version we've had in 15 years. And I must
admit myself that learning new special tricks is getting difficult at my
age, so it is better to invest efforts to keep things as simple as
possible. (Younger guys learning the system afresh will also benefit from
More information about the isabelle-dev