View the object most likely desired.
If it's a keyboard command, review the command.If it's the kind of term that's likely to refer to an object, then try to view that object.
If it can be used as an identifier in ML then: View a scratch copy of the first definition of this identifier if it's defined in an ML object.
If it's a pf term inference step, then pop up an analysis of the step: first try to break down
"<tac> THEN <tac>" s, then break down"<tac> ...." s, then start breaking down other tactics, perhaps all the way to primitive rules.Otherwise, try to view the ABS for the term.
If DIRECTION is reversed (by
If it's a keyboard command, show the command definitions mentioning it.IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.htmlIf it's an object reference to a theorem, find the proofs that cite it.
If it's an object reference to a definition of a non-system operator, find the definitions that mention it.
If it's an ML global id, then find the other ML globals whose definitions mention it.
Otherwise, if an instance of a non-system operator, find the definitions that mention it, like
`opdefs' .