PROVE : MEXPR

PROVE is a top-level command.
Start a new proof of a given wff.
The command format for PROVE is:

 <n>PROVE        WFF  PREFIX    NUM 
"GWFF0-OR-LABEL" "SYMBOL" "LINE"


The arguments have the following meaning:
WFF : Prove Wff
PREFIX : Name of the Proof
NUM : Line Number for Theorem

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage