[isabelle-dev] Proposal for localized interpretations

Makarius makarius at sketis.net
Sun Oct 12 20:46:03 CEST 2014

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



More information about the isabelle-dev mailing list