Re: [isabelle] Re-interpretation of locales does not generate abbreviations

Hi Peter,

This feature has been discussed already twice this year on the mailing list:

Clemens' locale implementation paper describes this as a feature, because it allows certain types of cyclic locale hierarchies, so I would expect that it won't change.


On 13/11/13 19:40, Peter Lammich wrote:
I encountered the following odd behaviour:
When interpreting a locale with a prefix, the expected abbreviations are
only generated if the locale has not been interpreted before with the
same parameters.

This feature is quite confusing, as it makes modular design more
difficult: If you need an instance of a locale for your theory, you must
make sure that none of the theories you are importing has already
instantiated this locale, and otherwise use the other theory's

Is there any workaround, or plans to change this behaviour? [Or good
reasons to keep it as is?]


locale foo begin
   definition "bar \<equiv> True"

interpretation p1!: foo by unfold_locales
interpretation p2!: foo by unfold_locales

term (* Does not exist! *)


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