[isabelle] removing abbreviations
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] removing abbreviations
- From: Christian Sternagel <c-sterna at jaist.ac.jp>
- Date: Wed, 13 Jun 2012 16:52:15 +0900
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:13.0) Gecko/20120605 Thunderbird/13.0
is it possible to remove an abbreviation. Currently I am using an
fixes P :: "'a => 'a => bool"
in order to fix the parameter (P) of another definition during document
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and