PBRIEF : MEXPR

PBRIEF is a top-level command.
This command prints a proof outline, hiding some lines.
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 PBRIEF shows
the lines included in the top levels of this hierarchy (to the
specified depth). PBRIEF is essentially a call to the command EXPLAIN
with the last line of the proof outline as the LINE argument (see help
for EXPLAIN). 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 PBRIEF is:

 <n>PBRIEF    DEPTH 
"INTEGER+"


The arguments have the following meaning:
DEPTH : Depth to Show

TPS documentation homepage


PBRIEF : TPS-FILE

PBRIEF is a file.
Defines the commands PBRIEF, EXPLAIN, BUILD-PROOF-HIERARCHY and PRINT-PROOF-STRUCTURE
/home/theorem/tps/bin/pbrief.fasl is part of module OTLNL.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage