[isabelle-dev] Find_Theorems interface

[Makarius]

On 13/11/2021 18:02, Peter Lammich 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.

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

The isabelle-dev repository is already for Isabelle2022.

If you want anything in Isabelle2021-1, you need to show me a changeset
(result of "hg export" wrt. a clone of
https://isabelle.sketis.net/repos/isabelle-release).


	Makarius