Re: [isabelle] Search in the whole Isabelle Library



On Mon, 1 Nov 2010, Brian Huffman wrote:

The idea is that you could go ahead and say "import qualified Library" at the top of your theory file, and it would bring all of the theorems from that theory into scope (and make them available for find-theorems, auto-solve, etc.) but it would not bring any more unqualified constant names into scope, or import any notations or other syntax. Any constants imported in this way could only be referred to by their fully-qualified names, as if they had been hidden by the "hide_const (open)" command. The point is that a qualified import should not affect the parsing of terms in your theory in any way.

I think such a feature would let you do all the kinds of theorem searching you want to do, plus it would be useful in lots of other situations, too.

Maybe some of the other developers could comment on how difficult this might be to implement.

This is a recurrent theme on isabelle-users or isabelle-dev for several years already. It is indeed difficult, but we are moving towards more or less exactly that for some years, getting closer after each round of reforms and cleaning up legacy features that are in the way.

It will work via the advanced infrastructure of local theories (and global specifications will be a special case). Most likely, this means that once the infrastructure is up and running, packages that are not "localized" would still emit their global declarations.


	Makarius





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