Re: [isabelle] LaTeXsygar (bug or feature?)

Dear Alfio,

it does process them everywhere where Isabelle pretty-prints.

In your example below, Isabelle’s pretty printer is only active for the antiquotation “term”. If you were to write @{thm silly_def} in the same text block, it would show the set comprehension as you expect.

The literal proof text above the “text {*” block is printed exactly as written without any pretty printing.

What I usually do for papers is to use only antiquotations and no literal proof text.


On 03.12.2013, at 10:10 pm, Alfio Martini <alfio.martini at> wrote:

> Dear Users,
> It seems that LaTexSugar does not process set expressions when
> they occur in function definitions, meaning {x | P} instead
> of {x. P}. Is this behavior intended?
> I prepared a small example theory showing what I mean:
> theory Test
> imports Main "~~/src/HOL/Library/LaTeXsugar"
> begin
> datatype fool = Fool
> fun silly::"fool ⇒ nat set" where
>  "silly Fool = {x. x≤7}"
> text{*
> In the above function definition,  the set expression on the
> right side of the equation is not processed by LaTeXsugar, while
> here, @{term "{x. x≤ 7}"} it is.
> *}
> end
> Best!
> --
> Alfio Ricardo Martini
> PhD in Computer Science (TU Berlin)
> Lattes:
> Associate Professor at Faculty of Informatics (PUCRS)
> Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
> 90619-900 -Porto Alegre - RS - Brasil


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

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