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