Hi Clemens, >> 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
>> 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.
It should not modify B at all -- with the restriction that ad-hoc
contexts currently may leak nontheless in certain situations (cf.
Makarius' statement).
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
