EditorDoc Sections Nuprl Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
`show' kbd_view_cases

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 `{(c-w)(m-w)(c-i)}') then it does a "backwards" lookup up sorts on certain kinds of expressions.

If it's a keyboard command, show the command definitions mentioning it.

If 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'.

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
EditorDoc Sections Nuprl Doc