Re: [isabelle] Retrieving context from theory

On Tue, 29 May 2012, Steve Wong wrote:

I just have a quick question: what is the proper way to grab the context
from a theory in ML? Is it ProofContext.init_global thy?

This is only init the global context, taking thy as a starting point, and leaves the question from where to get thy in the first place. Normally you get the proper local context structurally from the mechanisms to define new Isar language elements, e.g. method_setup.

See also the implementation manual, which has a lot to say about Isar contexts.

See also examples of existing user-defined language elements (proof methods, definitional packages etc.).


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.