Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Retrieving context from theory

Email Gateway (Aug 18 2022 at 19:58):

From: Steve Wong <s.wong.731@gmail.com>
Hi

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?

Thanks!

Steve

Email Gateway (Aug 18 2022 at 19:58):

From: Makarius <makarius@sketis.net>
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.).

Makarius

Last updated: Apr 20 2024 at 01:05 UTC