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