PRINT-OBTREE-NODE : WFFOP

PRINT-OBTREE-NODE is a wff operation.
Print out the given obligation in detail. If no
obligation is given, then the first open obligation
in the current obligation tree is used. See the flag
DEFAULT-OB-DEEP.
 
The calling scheme for PRINT-OBTREE-NODE is:

(PRINT-OBTREE-NODE NAME)
"SYMBOL-OR-INTEGER"


The result is of type MATINGSTREE.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage