[isabelle-dev] Find_Theorems interface

[Peter Lammich]

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