Hi all, after 3bfa28b3a5b2 (followed-up by AFP d058960a13d6) the matter of affairs with specification packages is as as follows:
The prototypical specification interface is of shape
val add_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 corresponding package is supposed to provide a morphism lifter for
results
val transform: morphism -> result -> result
The local theory stemming from add_specification may still contain
hypothetical results of the specification construction (I left this
untouched contrary to an idea I have expressed earlier on this
mailinglist); to get a proper close-up, there is a set of combinators:
* Local_Theory.subtarget_result for regular nested local theory;
* Named_Target.theory_map_result for global specifications;
* Overloading.theory_map_result for global overloaded specifications;
* Class.theory_map_result for global overloaded specifications relating
to type class instantiation.
Hence various *_global variants for specification packages have been
removed.
What I have left untouched are the various variants of primrec. Is there
still an ongoing work or plan to get rid of the old datatype / primrec
layer, or at least to have that retreat further? Otherwise I would have
a closer look a it to get an idea what can be done there.
Cheers,
Florian
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
