How to make find_theorems more specific

I am trying to find a theorem in Isabelle (2021) to the following effect:

lemma "A ⟹ B ⟹ A ∧ B"

So far, I have tried to use the following pattern:

find_theorems "_ ⟹ _ ⟹ _ ∧ _"

but it obviously returns a lot of results, as the pattern is too abstract. The various placeholders _ can represent very different things from one another.

I was wondering if there is any way to be more specific in the search, to express that some of the placeholders are the same. For example, can the following hypothetical example be achieved in Isabelle's search facilities?

find_theorems "_1 ⟹ _2 ⟹ _1 ∧ _2"

(indicating that all _1s are the same variable, all the _2s are the same etc.)

Solution

As I mentioned in my comment, find_theorems also take patterns as arguments similar to is. So anything of the form '?' followed by a string (and optionally a number [1]) can be used.

find_theorems "?A \<Longrightarrow> ?B \<Longrightarrow> ?A \<and> ?B"
(*
  "?A ⟹ ?B ⟹ ?A ∧ ?B"

found 1 theorem(s):
•  HOL.conjI: ?P ⟹ ?Q ⟹ ?P ∧ ?Q
*)

[1] with the usual caveat that "?A0" and "?A" refer to the same pattern.