This is an old revision of the document!
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