Isabelle/HOL Support Wiki

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

• 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.
• name: ident – searches for theorems that include ident in their name
• -name: ident – searches for theorems that do not include ident in their name