Re: [isabelle] where



Am 20.12.2013 um 20:48 schrieb Tobias Nipkow <nipkow at in.tum.de>:

> 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.

Jasmin





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