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.