> This is the proper season to start thinking about the coming release.
> We still have a few weeks ahead to consolidate in the usual way. I guess
> there will be a public Isabelle2016-RC0 just before Christmas or before
> New Year, to give people a chance to test it during the holidays.
>
> Are
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
