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
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