Hi Clemens,
> I didn't have time to look at your patches, and since I only have
superficial knowledge of instantiation contexts I didn't fully
understand the example either. I guess though that the purpose of these
global interpretations is to propagate some constant declarations into
the
Hi Florian,
I didn't have time to look at your patches, and since I only have superficial
knowledge of instantiation contexts I didn't fully understand the example
either. I guess though that the purpose of these global interpretations is to
propagate some constant declarations into the
Hi Clemens,
I have found a potential example for global interpretation into
instantiation in the existing Isabelle sources.
The example is presented in the attached patches, which can be applied
in alphabetical order on top of 32a530a5c54c.
The first patch experimentally introduces a
