[isabelle-dev] Proposal for localized interpretations

[Makarius]

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.


 	Makarius