Re: [isabelle] named theorems in Isabelle/ML

On Fri, 5 Dec 2014, Christian Sternagel wrote:

how do I imitate addition and retrieval of named theorems in Isabelle/ML. More specifically, to obtain all theorems in a named theorem bundle "a" I currently do

 Proof_Context.get_thms ctxt "Theory_Name.a"

This works, but it feels strange to add this Theory name prefix (although it would not be strictly necessary, I like to avoid potential clashes).

Moreover, how do I add new theorems to an existing bundle? I.e., the equivalent of

 declare some_thm [a]

in Isabelle/ML?

(Back to the start of this thread.)

The wording above confuses me.

Did you actually mean "bundle" in the formal sense of a bundle as defined by the 'bundle' command?

A "named theorem" is just a specific implementation of a "dynamic fact". A fact is a list of thm, and a dynamic fact a function that produces such a thm list from the context. No "bundle" here.


          1,070,206 people so far

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