Email Gateway (Aug 19 2022 at 08:05): Email Gateway (Aug 19 2022 at 08:05):From: Gottfried Barrow <gottfried.barrow@gmx.com>
So you might think, or me, that there's really only two
non-alpha-greek-numeric characters available for separating words in
identifiers: tick and underscore.
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.
--GB
theorem 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.
isub'forSpace.jpg
Last updated: Nov 21 2024 at 12:39 UTC