[isabelle-dev] Interpretation in arbitrary targets.
ballarin at in.tum.de
Thu Apr 18 21:42:26 CEST 2013
OK, then we agree on this.
Please let me know if you need to make changes to locales.ML. I want
to make sure that routes out of certain quirks there don't get blocked
Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:
> 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
>>> 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.
> Makarius' statement).
> PGP available:
More information about the isabelle-dev