[isabelle-dev] Interpretation in arbitrary targets.

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Wed Apr 24 19:16:38 CEST 2013

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

Still one thing to add:


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.



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

More information about the isabelle-dev mailing list