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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and