[isabelle-dev] Interpretation in arbitrary targets.

[Clemens Ballarin]

Hi Florian,

> I still see us disagree on how far the local theory game can be driven
> wrt. interpretation, nevertheless I can imagine that there is an
> intermediate road map which we can agree on:
>
> * Extend sublocale for use within locale targets s.t.

This is fine with me.  Will this work for named targets including  
classes or just locales?

> Rationale: We have 30 occurences of sublocale in HOL/*.thy and 80%   and
> more occur with the pattern

That's not very much.  In any case, in future, I would prefer a  
discussion starting from the problem towards a solution, not from a  
solution to the actual problem.

> * Equip interpretation in non-theory targets to allow confined,
> non-persistent interpretations.
>
>   context B
>   begin
>
>   interpretation EXPR
>
>   end
>
>   would not add a dependency to B.

Here, it's not clear whether the interpretation just wouldn't add a  
dependency, or wouldn't modify B at all.

Please clarify.

Clemens