| 1.
|
Their are several commands for raising objects related to the point-term.
| `vop'
|
will raise the definition of the operator of the point term, if there is one.
|
|
|
| `vdf'
|
will raise the DISP object being used to display the point term, if there is one.
|
|
|
| `vob'
|
will raise the object named by the point term, if any.
|
|
|
| `show'
|
and `(cm-(mouseright))' will usually raise a likely related object, most often doing a `vop' or `vob'.
|
|
|
|
| 2.
|
If you know a prefix or substring of the objects you want to find, you can try name completion on an object reference, say of form [ob name], which will return a bunch of similar object references. `(c-&)' is name completion from a prefix; `(c-a)(c-&)' is full name completion.
doc for name completion
|
|
|
| 3.
|
There is a utility ObTracker that tracks recently opened or closed objects. See the MainMenu. To force a refresh of its status, `(mouseleft)' on "Refresh" or anywhere outside the whole term, or use `(c-z)' anywhere in the window.
The main body of the term will be a listing of various objects, broken into classes.
The user can also force the persistent tracking of specific objects by clicking on their names with Notice (and Forget undoes it).
For explanation of annotations and options ob tracking MENU.
|
|
|
| 4.
|
The LibSearch button in MainMenu and ObTracker will raise a macro for some ML code that will search the library for objects satisfying a condition expressed in ML; click on it now. Fill in the condition slot, and execute with `(c-z)'. You will also find a little menu for inserting terms commonly used in such searches.
When the condition is applied to successive library objects, several ML ids will be bound to features of the object:
| obtok
|
the object name as a token
|
| kind
|
the object kind (possible values are in the menu)
|
| term
|
the contents of the object
|
| status
|
the verification status (possible values are in the menu)
|
(Use the Buttons button on the little menu to get documentation on what they do.)
The effect will be to raise a window containing references to the objects satisfying the condition.
|
|
|
| 5.
|
The button WhereIsIt? in MiscEditMenu (which can be raised with the MISC button in MainMenu) will show the names of objects that surround the object, or object referred to by the point, to which it is applied.
|
|
|
| 6.
|
Theorems, operator definitions, or rules that mention one or more specific operators can be found with the `thms', `{defs abses}', and `rules' commands. Definitions mentioning a given operator can also be found with `{(c-w)(m-w)(c-i)}'`show'.
|
|
|
| 7.
|
Lemmas with proofs explicitly citing a given lemma may be found with the WhoCites button in the proof editing menu PF, which is reachable from the MainMenu. Proofs citing a given lemma can also be found with `{(c-w)(m-w)(c-i)}'`show'.
|