IB : EDOP

IB is an editor command.
Instantiate a top-level universal or existential binder with a term.
 
The command format for IB is:

<Ed>IB TERM <<BDWFF>>
"GWFF" <<GWFF>>


The result replaces the current wff.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage