Re: [isabelle] LateXsugar broken?



Christian Doczkal wrote:
> Hello
>
>   
>> 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?
>   

I'm afraid that is not possible.

Tobias






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