[isabelle-dev] Interpretation in arbitrary targets.

[Florian Haftmann]

> But for the moment I will leave this aside anyway.

Still one thing to add:

http://isabelle.in.tum.de/repos/isabelle/rev/cb154917a496

avoids the odd reinit entirely, the critical lines being

> fun add_dependency locale dep_morph mixin export =
>   (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
>   #> activate_local_theory dep_morph mixin export

which add both an dependency *and* provide the facts in the context of
the current local theory.

Also, interpretation confined within blocks essentially boils down to
the singleton line

> val activate_local_theory = Local_Theory.target ooo activate_proof;

This is a great triumph of the »local everything« approach.

	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/20130424/89508f26/attachment.sig>