[isabelle-dev] Find_Theorems interface
kleing at unsw.edu.au
Sun Nov 14 01:51:09 CET 2021
I would welcome that change, happy for you to implement it (it doesn't have to be in 2021-1 from my side, I'll leave that up to you).
> On 14 Nov 2021, at 04:02, Peter Lammich <lammich at in.tum.de> wrote:
> I noticed that the Find_Theorems signature does not allow
> to decouple the filtering of the theorems from the obtaining of the
> unfiltered 'master' list of theorems.
> This yields to me being forced to duplicate the filtering code, just to
> filter over another source of theorems.
> My use-case:
> find_in_theorems <filters> in <fact_refs>
> to search in explicitly stated theorems, e.g.
> find_in_theorems "_+_" in algebra_simps
> Find_Theorems hides filtering, and only exposes combined function
> that filters all theorems from context.
> Proposed solution:
> add filter_theorems and filter_theorems_cmd to FIND_THEOREMS
> This has proved a very valuable tool for searching large fact
> databases, such as Hoare-rules in my Isabelle-LLVM project.
> Back then, I simply copy-pasted the code from find_in_theorems, but now
> stumbled over the code-duplication again as some changes are necessary
> to transition to 2021-1.
> Please advise me if I should simply commit such a change (and hopefully
> remember it on the next release, when I can use it from my tools (that
> work on release versions)), or how to get such a change in, or if the
> strong hiding is intentional, and I have to live with the code
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev