*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Search in the whole Isabelle Library*From*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Date*: Tue, 02 Nov 2010 15:50:17 +1100*In-reply-to*: <AANLkTimCDayGUvmZh94XPuaCvXXRVs8R5PfhyNcaypcw@mail.gmail.com>*References*: <265671288614154@web67.yandex.ru> <AANLkTimCDayGUvmZh94XPuaCvXXRVs8R5PfhyNcaypcw@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.1.9) Gecko/20100423 Thunderbird/3.0.4

Yours, Thomas. On 02/11/10 09:58, Brian Huffman wrote:

On Mon, Nov 1, 2010 at 5:22 AM, grechukbogdan<grechukbogdan at yandex.ru> wrote:Dear members of Isabelle group During my trip to Munich, we had an interesting discussion about search in the Isabelle Library. My point was that I would like to have a search in the whole library (not only imported theories), and we discussed some (complicated) ways for realization. I am thinking whether the following observation could simplify the situation. The naive way to use the current search facility in Isabelle to do global search would be to try to import everything. This, however, does not work directly: for example, if I try to write “imports Library” and than type lemma “(A :: real set)<B” I have an error, because “B” is reserved for something else. Moreover, even symbol “<” can have different meaning in different places of the library. In other words, Isabelle cannot parse (understand) mathematical expressions in this case.A feature I would like to see in Isabelle would be an "import qualified" option, like Haskell has. 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. - Brian

**References**:**[isabelle] Search in the whole Isabelle Library***From:*grechukbogdan

**Re: [isabelle] Search in the whole Isabelle Library***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Search in the whole Isabelle Library
- Next by Date: Re: [isabelle] Specializing types in locales
- Previous by Thread: Re: [isabelle] Search in the whole Isabelle Library
- Next by Thread: Re: [isabelle] Search in the whole Isabelle Library
- Cl-isabelle-users November 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list