EXPLAIN : MEXPREXPLAIN is a top-level command.
This command explains a line of a proof outline.
In particular, the command BUILD-PROOF-HIERARCHY builds
dependency information into a proof outline which allows
the proof outline to be viewed as a hierarchy of subproofs (see
help for BUILD-PROOF-HIERARCHY). The command EXPLAIN shows
the lines included in the levels of this hierarchy (to the
specified depth) starting at the level associated with the
specified line. Some flags which affect the printing include:
PRINT-COMBINED-UIS, PRINT-COMBINED-UGENS, PRINT-COMBINED-EGENS,
The command format for EXPLAIN is:
<n>EXPLAIN LINE DEPTH
The arguments have the following meaning:
LINE : Line to Explain
DEPTH : Depth to Show
TPS documentation homepage