[isabelle] UNdefining syntax?


In light of the recent thoughts on Multisets, I was wondering if it's possible to undefine previously defined syntax translations.

For instance:

  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?


Rafal Kolanski.

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