EXPLAIN : MEXPR

EXPLAIN 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,
and PRINT-UNTIL-UI-OR-EGEN.
The command format for EXPLAIN is:

 <n>EXPLAIN       LINE    DEPTH 
"EXISTING-LINE" "INTEGER+"


The arguments have the following meaning:
LINE : Line to Explain
DEPTH : Depth to Show

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage