Re: [isabelle] different fonts for various kinds of items in isatool-prepared documents?

On Fri, 3 Apr 2009, Andrei Popescu wrote:

I am trying to prepare a latex document with isatool, and was wondering whether there is a way to set particular fonts for different kinds of items, e.g.:
-- italic for schematic variables (appearing in theorems);
-- sans serif for constants
-- bold for types

(That would greatly improve readability.) 

In principle this could be done for anything is printed via document antiquotations, going through the Isabelle syntax engine. You can then modify the presentation of certain atomic entities via the internal concept of token translations.

This won't affect regular theory sources, though. This is because the document preparation system does not really understand the structure of the formal entities that it is typesetting.


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