[isabelle-dev] Interpretation in arbitrary targets.

[Makarius]

On Tue, 26 Mar 2013, Makarius wrote:

> Semantically, do you remember reasons why we did not consider it so far, or 
> was it just forgotton or lost in state-budget problems?

I now recall some aspects from the wild days of all that (2006/2007), when 
we built up that national debt.  (Unlike Cyprus we managed to reduce it 
over the years.)

At some point I was always speaking about "interpretation (in ...)", 
Florian made his 'subclass' command, and Clemens his 'sublocale'.  It was 
all moving forwards, but without full convergence.  So maybe we have a 
chance now several years later.


 	Makarius