[isabelle-dev] Proposal for localized interpretations
florian.haftmann at informatik.tu-muenchen.de
Mon Sep 15 21:20:43 CEST 2014
> Well, I am. My proposal is to kick out "interpretation.ML" and replace it with "local_interpretation.ML".
Well, if this works out, fine.
>> Of course to fully generalize we
>> would need a concept of »reconstructable« local theory, i.e. each
>> target would provide an operation reenter :: local_theory -> (theory ->
>> local_theory) option. Is it worth the effort? It appears very similar
>> to the ancient infamous reinit operation.
> Who is talking about more effort? Why not consider what I proposed at face value?
I was just thinking aloud whether the existing local theory
infrastructure would offer something here. That would be something like
this: »Go back in thought what you would have done within that local
theory at an ealier stage and transfer the hypothetical effect on the
former background theory to the current background theory.« Seems not
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 181 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev