Re: [isabelle] thms_containing

On Tue, 15 Apr 2008, Jeremy Dawson wrote:

> This function seems to have disappeared form a very recent development 
> version of Isabelle.  Or, rather, it seems it recently changed its name 
> to thms_containing_consts, since I apparently changed my own code 
> accordingly, but now it has disappeared completely.

This ancient way of indexing facts was both very slow to build, and in 
fact unused in the past few years.  Facts are now stored in a plain 
Facts.T table; the following example shows how the 'find_theorems' command 
retrieves facts from the context:

fun all_facts_of ctxt =
  maps Facts.selections
   (Facts.dest (PureThy.all_facts_of (ProofContext.theory_of ctxt)) @
    Facts.dest (ProofContext.facts_of ctxt));

The result is just a plain list, without any special indexing.

If you need special-purpose indexing you can use Theory.at_begin or 
Theory.at_end hooks to maintain a derived data structure, but this is not 
completely trivial.


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