`find_theorems` in the AFP

user_1308444 0
Viewed 113

How can I use the find_theorems mechanism to search the whole Archive of Formal Proofs (AFP)?

I have downloaded the archive to my machine, and I am able to import theories from it. For instance, if I write imports Kleene_Algebra.Kleene_Algebra_Models then all the theorems in that theory are successfully made available to me. But if I then type find_theorems <expression>, I only get search results from the specific theory I imported. What if I want to search the whole archive? For instance, perhaps somebody has proved a theorem that is useful to me, but I don't know what they called their theory.

isabelle
2 Answers

To put it plain and simple, you can't, unless you import the entirety of the AFP into your theory (which probably won't work).

I'm unsure whether someone is currently working on making what you want happen.

user_47769390

find_theorems only works with the loaded theories. You can use any text search tool if you have an idea of the theorem name. On macOS, the Splotlight Search (cmd + space) can be useful.

Admin1
Related