Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] where


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 04:18 UTC