[isabelle] Antiquotations and Syntax Annotations

Dear Isabelle Users,

When defining datatypes with syntax annotations, the usual commands @{term
"..."}, @{const "..."} present the
corresponding expressions with the alternative syntax, even if specified

For instance, assuming the declaration below

datatype 'a List =   Nil ("[]")
                   | Cons 'a "'a List" (infixr "#" 65)

we have the following:

@{term "Nil"}  produces "[]" (wanted "Nil")

@{term "Cons"} produces "op #" (wanted "Cons") [tried @{const "Cons"}, but
it does not work either]

@{term "Cons h t"} produces "(h::'a) # (t::'a List)" (wanted "Cons h t").

When I want types I use term_type or show_types.

Anyway, judging from the way the tutorial (section 4.1.1, definition and
discussion of "xor") I assume this kind of
control is possible with the available resources.

I could use @{text "..."}, but this would be plain and simple humiliation.

Thanks for any help on that!
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
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.