[isabelle-dev] Interpretation in arbitrary targets.

[Clemens Ballarin]

Quoting Lars Noschinski <noschinl at in.tum.de>:

> How is interpretation related to print_context? It seems that  
> neither interpret nor interpretation extends the context as  
> displayed by print_context?

I don't know the answer to that, but for a particular locale x you  
should be able to find all active interpretations in a context by

   print_interps x

Clemens