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
Here is another Isabelle test snapshot:
http://www4.in.tum.de/~wenzelm/test/Isabelle_23-Dec-2015
It contains an updated version of Poly/ML as an approximation of version
5.6 that David Matthews is preparing for the beginning of 2016.
After the Christmas break, there will be further moves
