Re: [isabelle] LateXsugar broken?


> Replace the "term" command by an antiquotation, eg
> text{* @{term "if a then b else c"} *}
> That should do the job.

OK, that does indeed work. I expected this to apply not only to
antiquotations but also to the theory itself. Using it this way
introduces notational inconsistencies as the terms have different fonts
in lemmas/proofs than they have in the text body. Is there a way to
extend the scope of these output transformations to the whole theory?

Christian Doczkal

Attachment: smime.p7s
Description: S/MIME cryptographic signature

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