# Re: [isabelle] UNdefining syntax?

On Tue, 11 Dec 2007, Rafal Kolanski wrote:
> 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?
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

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