ADD-BESTMODE : LIBRARYCMDADD-BESTMODE is a library command.
Add a mode for the specified theorem to the list in your
bestmodes.rec file. If the theorem and mode are already present in
the list (either in your directory or in another user's), you will
be asked to confirm the creation of a new entry. If they are already
present in your own directory, you will be given the option of
The command format for ADD-BESTMODE is:
<LIB>ADD-BESTMODE THEOREM MODE DATE TIME COMMENT
"SYMBOL" "SYMBOL" "SHORT-DATE" "INTEGER+" "STRING"
TPS documentation homepage