[isabelle-dev] Interpretation in arbitrary targets.

Clemens Ballarin ballarin at in.tum.de
Wed May 22 19:02:52 CEST 2013


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




More information about the isabelle-dev mailing list