[isabelle-dev] Proposal for localized interpretations

[Florian Haftmann]

> 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140915/76e29a9d/attachment.sig>