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
