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.

Cheers,
Gerwin

On 03.12.2013, at 10:10 pm, Alfio Martini <alfio.martini at acm.org> 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)
> www.inf.pucrs.br/alfio
> Lattes:  http://lattes.cnpq.br/4016080665372277
> 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.