[isabelle-dev] Interpretation in arbitrary targets.
florian.haftmann at informatik.tu-muenchen.de
Thu Apr 18 11:07:47 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?
it will work within locales, and thus within type classes.
>> * 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.
It should not modify B at all -- with the restriction that ad-hoc
contexts currently may leak nontheless in certain situations (cf.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 261 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev