[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