Re: [isabelle] LateXsugar broken?



Christian Doczkal wrote:
> Hello
>
> I have some minimalistic session containing the theory (importing Main
> was well had no effect)
>
> theory SugarTest
>   imports LaTeXsugar
> begin
>   term "if a then b else c"
> end
>
> According to the documentation (sugar.pdf) this should suffice to have
> the "if" "then" "else" typeset in sans serif fonts. Unfortunately
> neither this not any other syntactic sugar works with my Isabelle
> environment. (Isabelle2008)
>
> I uses the standard makefile generated by isatool mkdir and have only
> added SugarTest to ROOT.ML Can someone reproduce this? (Whole session is
> attached)
>
> Am I missing something or is this really not working?
>
>
>
>
>   
Replace the "term" command by an antiquotation, eg

text{* @{term "if a then b else c"} *}

That should do the job.

Tobias





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