[isabelle-dev] Interpretation in arbitrary targets.
makarius at sketis.net
Tue Mar 26 15:26:07 CET 2013
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
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 :-)
More information about the isabelle-dev