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.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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