TEST-INIT is a top-level command.
Initialize the flag TEST-THEOREMS to test all of the best
modes known to the library. By default, this will choose the first
mode listed for each theorem in the bestmodes.rec file; if you
choose to "use multiple modes" then it will test each theorem
with all of the modes listed for it in that file.
The command format for TEST-INIT is:


The arguments have the following meaning:
MULT : Use multiple modes for same theorem?

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage