[isabelle-dev] Interpretation in arbitrary targets.

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130418/e97b05ee/attachment.sig>