Re: [isabelle] Obtaining a list of theorems in ML



On Tue, 1 Sep 2015, Viorel Preoteasa wrote:

 For example, dynamically changing facts can be managed like this in
 Isabelle2015:

   named_theorems foo

   ML âfun get_foo ctxt = Named_Theorems.get ctxt @{named_theorems foo}â

 The user can now use attributes [foo add] or [foo del].  Your tool can use
 get_foo to see the current content in a given context.

This is a nice solution. Is there a way to also clear the foo content, without knowing what it contains?

That is the missing [foo only] that will probably emerge for the next release. For now, the implementation of Named_Theorems can be taken as an example how to do such things yourself.

An important ingredient is Local_Theory.add_thms_dynamic to expose certain context-defined fact content to the user by a specific name. If you don't like general Local_Theory programming interfaces, you can also do it a global theory like this:

  setup âGlobal_Theory.add_thms_dynamic (@{binding foo}, undefined)â

The "undefined" function accesses your tool-specific facts. You can maintain that in any way you like, e.g. via Generic_Data in the context.


	Makarius


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