User Tools
reference:theorem_search
Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision | ||
|
reference:theorem_search [2011/06/13 22:07] 178.26.109.100 created |
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. | ||
reference/theorem_search.1307995650.txt.gz · Last modified: 2011/06/13 22:07 by 178.26.109.100
Page Tools
