Re: [isabelle] LateXsugar broken?



Christian Doczkal wrote:
> 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.
>
>
>   
They don't use the same mechanism.

Tobias





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