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 <[email protected]> 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 > [email protected] > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
