Isabelle/HOL Support Wiki

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.

===== 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 (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.
  * ''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

=== 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.

Isabelle/HOL Support Wiki

User Tools

Site Tools

Page Tools