Re: [isabelle] removing abbreviations

> is it possible to remove an abbreviation. Currently I am using an
> auxiliary context
> context
>   fixes P :: "'a => 'a => bool"
> begin
> ...
> in order to fix the parameter (P) of another definition during document
> preparation.
> Thus I defined syntax for P (via notation) as well as the abbreviation
> abbreviation notP :: "'a => 'a => bool" where
>   "notP x y == not P x y"
> also with special syntax.
> However, after closing the context, the abbreviation is still active and
> but turns out to be too general, since, e.g., "~ (x = y)" is now also
> printed "notP (op =) x y", which was not intended. Any advise?

I guess the situation is similar to thread »syntax in auxiliary
contexts«: the handling of syntax declaration wrt. to the context
sandwich still needs fine tuning.

Apart from that, there is no way to remove an abbreviation:
abbreviations are managed monotonously.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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