> 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
very comfortable.
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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
