Re: [isabelle] where

On Fri, 20 Dec 2013, Jasmin Blanchette wrote:

Am 20.12.2013 um 20:48 schrieb Tobias Nipkow <nipkow at>:

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?

"where" is also a keyword, e.g. "fun f where ...". I guess that's where the formatting comes from.

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.