NAME : EDOP

NAME is an editor command.
Assign a label to the edwff, and replace the edwff with this label.
 
The command format for NAME is:

<Ed>NAME LABEL <<GWFF>>
"SYMBOL" <<GWFF>>


The result replaces the current wff.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage