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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
