Re: [isabelle] Antiquotations and Syntax Annotations

You can write @{term [source] "..."} and it checks and prints your term as you
gave it - unfortunately including the quotation marks. You can work around that
by setting the quotation marks temporarily to empty:


If you never want to see them, then you can of course do the above
\renewcommands globally.


Am 12/10/2012 13:50, schrieb Alfio Martini:
> 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
> otherwise.
> 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!

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