[isabelle] LaTeXsygar (bug or feature?)

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"
datatype fool = Fool

fun silly::"fool ⇒ nat set" where
   "silly Fool = {x. x≤7}"

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.

Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
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

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