Email Gateway (Aug 19 2022 at 13:01): Email Gateway (Aug 19 2022 at 13:01):From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,
Documents generated with Isabelle build tool
produce an hyphen instead of an underscore whenever the
later is used in identifiers and concrete syntax annotation.
I think this is (a bit) unfortunate as a choice for a default definition.
After a brief inspection of the isabelle.sty file, I added the
following workaround to my prelude.tex file:
def\isacharunderscore{\mbox{\_}}%
It works, but it I wonder if this is the proper way.
Thanks for any comments on that!
Email Gateway (Aug 19 2022 at 13:04):From: Makarius <makarius@sketis.net>
A more standard way is to use the high-level macro \isabellestyle, e.g.
\isabellestyle{literal} to get closer to what you write in the source
text. You can also try one of the tt forms.
Any attempt to change defaults will cause a major bloodshed among seasoned
users of the Isabelle document prepration system. It will disrupt
existing documents that assume certain styles implicitly.
Note that the small dash for rendering underscore emerged in 1996 as a
typographically correct way to represent the idea of separating parts of
identifiers in mathematical text, without making it look like "code".
Today the majority of people have given up the very idea of separation
altogether andPreferToWriteInCamelCaseEvenThoughThatIsHardlyReadable.
O tempora o mores!
Makarius
Email Gateway (Aug 19 2022 at 13:10):From: Tobias Nipkow <nipkow@in.tum.de>
Am 02/12/2013 05:04, schrieb Alfio Martini:
Dear Isabelle Users,
Documents generated with Isabelle build tool
produce an hyphen instead of an underscore whenever the
later is used in identifiers and concrete syntax annotation.I think this is (a bit) unfortunate as a choice for a default definition.
After a brief inspection of the isabelle.sty file, I added the
following workaround to my prelude.tex file:def\isacharunderscore{\mbox{\_}}%
For tutorials, where every character matters, I do (more or less) exactly that
and it works fine. In standard papers I quite like the "-".
Tobias
It works, but it I wonder if this is the proper way.
Thanks for any comments on that!
Last updated: Apr 25 2024 at 12:23 UTC