[isabelle-dev] Interpretation in arbitrary targets.

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Apr 18 11:07:47 CEST 2013

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).



PGP available:

-------------- 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>

More information about the isabelle-dev mailing list