To find the definition of a mathematical operator: "Definitions"

Find a page containing an instance of it, then click the "Definitions" button in the corner.
Then scroll through the resulting Definition Cascade and find the definition.

To find the definitions used in a Section : "Definitions"

Use this button on the Main Page for a Section or on a Definition Cascade belonging to the section.

To find the documentation for a primitive operator: " < image of operator > "

Find a page containing an instance of it, then click the image of the operator appearing at the bottom of the page.

To find the thms and defs using an operator: "Definitions" "Def" "WhoCites"

Find its definition as explained above, then click on the "Def" at the individual definition shown for it. This will take you to a page containing that definition at the top of a Definition Cascade . Click the "WhoCites" link in that page.

To find the lemmas cited by a given proof: "Lemmas"

On any inference step node for the proof, click "Lemmas" if it appears.

To see a proof: "Thm" "PrintForm"

Click on the "Thm" at the statement of a theorem, which will take you to the top Inference Step . You can navigate through the proof step-by-step or you can view the whole proof in postscript with the "PrintForm" link in the corner of any step within the proof.

The printform has no links, so the only way to analyze the contents of a proof with the browser is through the individual proof steps.

To navigate a proof: " < subgoal number > " or " < ancestor address > "

Click on the number of a subgoal within an inference step to go down into it, or inside the address at the top left of the page to go up to an ancestor.

To find the list of objects in a section: " < section name > "

Click the link in the corner of any page belonging to the section bearing the section name. It is possible that no listing of the section objects has been provided, and you may simply be given an introductory document for the section instead.

To find the sections a section depends on: " < section name > " "Sections"

Click the "Sections" link in the corner.