[isabelle-dev] Interpretation in arbitrary targets.
ballarin at in.tum.de
Wed Apr 17 22:18:13 CEST 2013
> 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
> interpretation EXPR
> 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.
More information about the isabelle-dev