[isabelle-dev] Interpretation in arbitrary targets.

Makarius makarius at sketis.net
Wed Mar 27 11:05:20 CET 2013

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.


More information about the isabelle-dev mailing list