[isabelle-dev] Proposal for localized interpretations

Makarius makarius at sketis.net
Mon Oct 13 23:38:48 CEST 2014

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 

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
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.



More information about the isabelle-dev mailing list