[isabelle-dev] Find_Theorems interface

[Gerwin Klein]

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).

Cheers,
Gerwin

> On 14 Nov 2021, at 04:02, Peter Lammich <lammich at in.tum.de> wrote:
> 
> Hello,
> 
> 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
> 
> Problem:
> 
>  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
> signature.
> 
> Background:
> 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
> duplication.
> **********************
> 
> --
>  Peter
> 
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev