[isabelle-dev] Interpretation in arbitrary targets.

[Clemens Ballarin]

Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:

> Let those thoughts sink further few days.  If there is no veto until Apr
> 7th, I would go ahead to turn the patches upstream.

Well, here is my veto.

I don't see that much of a discussion has taken place yet, and I am  
very unhappy about the concepts and terminology you are trying to  
introduce.  As you are aware, I do have another job, which makes  
responding as quickly as you would like impossible.  I do hope,  
though, that we can get this discussion further within this month.

Clemens