But then you, or I, would be wrong because of \<^isub> and \<^isup>. These would bump up the use of tick and underscore to 6 available characters.
Well, once it's occurred to you, or me, that \<^isub> and \<^isup> can be useful for naming tricks, like creating space in a more subtle way, then surely you think, or I think, there are other possibilities for using \<^isub> and \<^isup> for identifier tricks.
The solution is simple. I introduce a function, such as "be bounded by", in a LaTeX theorem environment, named using spaces. It's understood that "be bounded by" will be named in Isar with different characters to separate the words. And, after all, the Isar code will be shown to them. It's not too much to expect that people will make the connection between "be bounded by" in some formal-non-formal natural language proof, and the "be_bounded_by" in the Isar proof (or be_bounded_by with something else in place of "_").
And typing \<^isub>' isn't that bad with the "-_" shortcut.It's also not a trivial thing to have subscripts available for use in identifiers, in general.
I attached a screen shot of the Verbatim environment with \<^isub>' being used for spacing. It looks good in jEdit too. These kind of options are always good to have, even if you decide not to use them.
--GBtheorem emS\<^isub>'is\<^isub>'unique: "u = emS \<longleftrightarrow> (\<forall>x::sT. \<not>(inS x u))"
apply(auto) oops Let A be'bounded'by b. Let A be\<^isub>'bounded\<^isub>'by b.
Description: JPEG image