TEST-THEOREMS is a flag or parameter.
A list of pairs; the first of each pair is the name of a theorem;
the second is the name of a mode. If the mode name is NIL, TPS will
attempt to choose a mode from the list of best modes in the library.
This flag is used by the command TPS-TEST, and can be set automatically by
the command TEST-INIT.

The default setting is a sample list of two standard TPS exercises, both
to be run in mode ML (also standard in TPS). If you set this flag yourself,
beware of unexported symbols --- which is to say, make sure that the
symbols you use are all in the USER package (this is particularly
necessary if you are using library theorems which are not yet loaded
into TPS, or they may end up interned in the wrong package). If in doubt,
put "USER::" before all symbols, thus:

(setq test-theorems '((user::thm30 . user::mode-thm30) (user::x2112 . user::ml)))

You can use the flag TEST-MODIFY to alter modes on the fly as TPS-TEST runs.
See the help messages for TEST-INIT and TEST-MODIFY for more information.
It belongs to subjects MAINTAIN .
Its default value is ((X2106 ML) (X2108 ML))
Its current value is ((THM15A MODE-THM15A-1) (THM15B MODE-THM15B-PR97-A) (THM30 MODE-THM30-MSV) (THM104 MODE-THM104-MSV) (THM112 MODE-THM112-MSQ) (THM112C MODE-THM112C-MSQ) (THM115 MODE-THM115-PR97A) (THM117C MODE-THM117C-MSQ) (THM129 MODE-THM129-MSV) (THM131 MODE-THM131-MSV-A) (THM134 MODE-THM134-MSQ) (THM135 MODE-THM135-MSV-A) (THM143A MODE-THM143A-1) (THM301 MODE-THM301-MSQ) (THM301A MODE-THM301A-MSQ) (X5200 MODE-X5200-MSQ) (X5205 MODE-X5205-MSQ) (X5304 MODE-X5304-MSQ) (X5305 MODE-X5305-MSQ) (X5308 MODE-X5308-MSQ) (X5310 MODE-X5310-A) (THM15B MODE-THM15B-PR97-A)).

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage