Hi all, as of 82f57315cade (followed-up by AFP bf62184), the still occasionally seen Local_Theory.reset invocations are gone, conveniently replaced by Local_Theory.subtarget_result.
I'm considering pushing that even further: specification tools should by contract provide a »clean« definitional extension without any artefacts of the internal construction leaking out, i. e. val specification: spec -> local_theory -> result * local_theory where »spec« is the input specification and »result« a characterization of the definitional extension with enough information to build on it in derived tools; the resulting local_theory can be continued on directly -- all internal construction steps are hid in a local subtarget. The corresponding package is supposed to provide a morphism lifter for results val transform: morphism -> result -> result hence exporting up through nested context is trivial. This would also open up the possibility to get rid of the still seen *_global variants for specification tools: using a combinator Named_Target.theory_map_result: (morphism -> 'a -> 'a) -> (local_theory -> 'a * local_theory) -> theory -> 'a * theory any Package.spec_global can be trivially inlined as Named_Target.theory_map_result Package.transform (Package.spec …) So much my current understanding of affairs. Cheers, Florian
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev