Re: [isabelle] Modifying syntax of imported theories?

On Thu, 2 Apr 2009, Dr. Brendan Patrick Mahony wrote:

Regarding no_syntax and no_notation, they have the provoking property that it is hard to get the revoked syntax to stay revoked.

This happens uniformly for all global declarations (at the immediate theory level), e.g. declare foo [simp del]

Or else the theory import could be a bit smarter and not merge in a theory that is imported by another imported theory.

Locales already work differently: instead of maintaining (and merging) data, they manage declarations on data (update functions). So here you would get a potentially more convenient behaviour: the last declaration of notation or no_notation will take effect.

I have occasionally pondered the question if one could achieve a similar mode of operation at the global level as well, without breaking every existing theory out there.

If you unthinkingly include Set.thy, or anything else that directly imports Set.thy, all the ugly notation is right back where you don't want it. This means you frequently can't use the imports list that best describes or hints at the subject matter of a new theory.

Normally you should never import anything below theory Main, or you will inevitably participate in the quite delicate bootstrap process of Main HOL. Strange effects can happen when primitive theories of HOL are merged via different paths.


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