[isabelle-dev] Proposal for localized interpretations

[Makarius]

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


 	Makarius

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