Re: [isabelle] named theorems in Isabelle/ML



Sorry for the confusion (in fact, awareness of the potential confusion seeped in directly after pressing the "send" button of my email client). To clarify, what I meant was "collection" of theorems (and after your explanation I guess what I really meant was the "dynamic fact" implementation corresponding to the "named_theorems" command).

cheers

chris

On 12/08/2014 05:11 PM, Makarius wrote:
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.


     Makarius

----------------------------------------------------------------------------

                   http://stop-ttip.org  1,070,206 people so far
----------------------------------------------------------------------------





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