reference:theorem_search

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.

reference/theorem_search.txt · Last modified: 2011/06/29 12:50 by 131.246.161.187