[isabelle-dev] Interpretation in arbitrary targets.

[Makarius]

On Sun, 24 Mar 2013, Florian Haftmann wrote:

> There is a series of minimal invasive patches to generalize
> »interpretation« / »sublocale« to »interpretation« in arbitrary targets,
> not just theories and locales. The patches are inspectible at
>
> 	http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation

OK, lets see if we get some actual work done here ...


In the first round of just eye-balling this looks formally correct to me. 
(I will look more closely a bit later.)

Semantically, do you remember reasons why we did not consider it so far, 
or was it just forgotton or lost in state-budget problems?  We have a 
little bit of budget now after the release and towards the summer, but we 
need to stay within a reasonable range of complexity.

Clemens Ballaring might also have an informed opinion on that -- I've just 
seen some locale-related activitity by him (e.g. c3eb0b517ced).


> * Amend the instantiation target not to choke on abbreviations stemming
> from interpretations.

Most problems of computer-science can be reduced to abbreviations within 
local contexts in Isabelle :-)


 	Makarius