Re: [isabelle] LateXsugar broken?

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


> I'm afraid that is not possible.

What is the fundamental difference between rendering a term in the
theory as latex output and rendering a term in an antiquotation as latex
output? I was expecting that both use the same mechanisms.

Christian Doczkal

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

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