ccccccccccccc
Locate and display an object by its short name. For instance locating the identifier "nat" gives you back the definition of natural numbers, and locating "plus" returns several (axiomatic and concrete) definitions of the sum.
Given a closed statement G of the form \forall x1:T1...xn:Tn.body returns all theorems in the library whose conclusion is a generalization of body, that is all theorems which can be used (as a last step) to prove G (for tecnical reasons, the actual result may be a superset of the expected one).
