Email Gateway (Aug 19 2022 at 13:04): Email Gateway (Aug 19 2022 at 13:04):From: Tobias Nipkow <nipkow@in.tum.de>
Hi,
I wonder about the way in which "where" is printed by the Isabelle document
preparation system. According to the isar-ref manual, "where" is an attribute
like "OF" and "of", but in tex documents "where" becomes \isakeyword{where}
whereas "of" and "OF" are unmodified. Is there some subtle distinction I should
be aware of?
Thanks
Tobias
Email Gateway (Aug 19 2022 at 13:05):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
"where" is also a keyword, e.g. "fun f where ...". I guess that's where the formatting comes from.
Jasmin
Email Gateway (Aug 19 2022 at 13:47):From: Makarius <makarius@sketis.net>
There are indeed some strange tricks from the depth of time, to allow a
minor keyword of the outer syntax to be used as plain name within the
"args" syntax of attributes. That is a historical accident, and I would
not do it again today: Isabelle sub-languages should be cleary separated.
Nonetheless there is an easy workaround for books or papers where "where"
is meant to be really just a plain name, not a keyword disguised as name:
simply put double quotes around it, and use a Isabelle/latex style that
suppresses the quotes.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC