Isabelle/HOL Support Wiki

By typing C-c C-f, you get a search prompt. You can search for (a combination of) several things:

• pattern – searches for theorems whose expressions match the given pattern.
• intro – searches for theorems which can be applied with rule, i.e. that fit the current goal.
• dest – searches for theorems which can be applied with drule, i.e. whose major premise fits one of the assumptions.
• elim – searches for theorems which can be applied with erule
• name: ident – searches for theorems that include ident in their name
• -name: ident – searches for theorems that do not include ident in their name

Given the goal

  length (l1 @ l2) = length l1 + length l2

searching for “_ @ _” and intro each yield a list of theorems that fit. Combining both, i.e. searching for “_ @ _” intro, yields exactly the theorem wanted.