[isabelle-dev] Interpretation in arbitrary targets.
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