[isabelle] removing abbreviations



Dear all,

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?

cheers

chris





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