This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
reference:theorem_search [2011/06/13 22:15] 178.26.109.100 |
reference:theorem_search [2011/06/29 12:50] (current) 131.246.161.187 |
||
---|---|---|---|
Line 2: | Line 2: | ||
By typing ''C-c C-f'', you get a search prompt. You can search for (a combination of) several things: | 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 (method)|rule]]'', i.e. that fit the current goal. | * ''intro'' -- searches for theorems which can be applied with ''[[rule (method)|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. | * ''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 include ''ident'' in their name | ||
* ''-name: ident'' -- searches for theorems that do not include ''ident'' in their name | * ''-name: ident'' -- searches for theorems that do not include ''ident'' in their name | ||
+ | |||
+ | === Example === | ||
+ | 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. |