[isabelle-dev] Proposal for localized interpretations

[Makarius]

On Sun, 12 Oct 2014, Makarius wrote:

> On Tue, 16 Sep 2014, Makarius wrote:
>
>>  On Fri, 5 Sep 2014, Jasmin Christian Blanchette wrote:
>> 
>> >   I would like to propose either replacing the old mechanism by the new 
>> >   one
>> >   or having both live in parallel in "Pure". It is certainly not perfect,
>> >   but it is IMO an improvement over the statu quo. What do you think?
>>
>>  I still need to catch up with this important thread, but I am presently
>>  not well-connected.  I will come back later, when I have studied the
>>  situation carefully.
>
> I have picked up this old thread, and started to rework the old 
> Haftmann-Wenzel version wrt. the new Blanchette version.  Stay tuned ...

See now Isabelle/4e4a4c758f9c where the old interpretation.ML is already 
removed.

In the earlier changesets, the various uses of interpretation.ML and 
local_interpretation.ML are converged towards the new plugin.ML -- the 
main transition point is:

changeset:   58657:6c9821c32dd5
user:        wenzelm
date:        Mon Oct 13 18:45:48 2014 +0200
description:
Local_Interpretation is superseded by Plugin with formal Plugin_Name 
management, avoiding undeclared strings;


I did not intend to push everything through in the first round, but it 
worked out smoothly as far as I can see at the moment.


 	Makarius

----------------------------------------------------------------------------
                               http://stop-ttip.org
----------------------------------------------------------------------------