apropos
DB.apropos : term -> data list
Attempt to find matching theorems in the currently loaded theories.
An invocation DB.apropos M collects all theorems, definitions, and
axioms of the currently loaded theories that have a subterm that matches
M. If there are no matches, the empty list is returned.
Failure
Never fails.
Example
> DB.apropos (Term `(!x y. P x y) ==> Q`);
<<HOL message: inventing new type variable names: 'a, 'b>>
val it =
[(("bool", "LCOMM_THM"),
(⊢ ∀f. (∀x y z. f x (f y z) = f (f x y) z) ⇒
(∀x y. f x y = f y x) ⇒
∀x y z. f x (f y z) = f y (f x z), Thm,
Located
{exact = true, linenum = 4445, scriptpath =
"$(HOLDIR)/src/bool/boolScript.sml"})),
(("cardinalityCore", "CARD_EQ_IMAGE"),
(⊢ ∀f s.
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒ cardeq (IMAGE f s) s,
Thm,
Located
{exact = true, linenum = 2268, scriptpath =
[...Output elided...]
Comments
The notion of matching is a restricted version of higher-order matching.
For finer control over the theories searched, use DB.match.