DELETE : LIBRARYCMD

DELETE is a library command.
Delete an object from the library.

If more than one library object of this name is stored in
the library, the user is prompted to disambiguate.
 
The command format for DELETE is:

<LIB>DELETE NAMES TYPE
"SYMBOLLIST" "LIB-ARGTYPE-OR-NIL"

TPS documentation homepage


DELETE : MEXPR

DELETE is a top-level command.

Delete lines from the proof outline.
The command format for DELETE is:

 <n>DELETE      DEL-LINES 
"EXISTING-LINELIST"


The arguments have the following meaning:
DEL-LINES : delete lines

TPS documentation homepage


DELETE : TESTCMD

DELETE is a test-top command.
Delete a saved searchlist or mode (equivalent to the library
command DELETE.
 
The command format for DELETE is:

<TEST>DELETE NAME TYPE
"SYMBOL" "LIB-ARGTYPE"

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage