> 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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
