Re: [isabelle] LateXsugar broken?



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


-- 
Regards
Christian Doczkal

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



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