Email Gateway (Aug 18 2022 at 11:07): Email Gateway (Aug 18 2022 at 11:07):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Hello,
In light of the recent thoughts on Multisets, I was wondering if it's
possible to undefine previously defined syntax translations.
For instance:
definition
single :: "'a => 'a multiset" ("{#_#}") where
"{#a#} = Abs_multiset (lb. if b = a then 1 else 0)"
Let's say I want {#x#} to mean something else now, or I am not happy
with that definition and wish to redefine it (like Tobias did in a
previous post). Is it possible to forcibly remove it?
Sincerely,
Rafal Kolanski.
Email Gateway (Aug 18 2022 at 11:08):From: Makarius <makarius@sketis.net>
Since the theory context works in a monotonic fashion all the time, you
cannot remove logical content. What you can do is introduce new
definitions that override old entries in the name space (beware of
potential confusion!). The ``hide const ...'' facility might be
occasionally helpful to suppress former name space accesses.
Moreover, starting with Isabelle2007, concrete syntax is managed in a more
flexible way, analogous to simp add/del declarations. Cf. the commands
'notation' and 'no_notation', which can be used like this:
no_notation single ("{#_#}")
-- "NB: need to specify original notation here, to delete it reliably"
notation my_single :: "'a => 'a multiset" ("{#_#}")
-- "whatever syntax you like"
Makarius
Last updated: May 03 2024 at 08:18 UTC