PRESS-DOWN : INFO

PRESS-DOWN is a flag setting or other piece of information.
A setting for TEST-NEXT-SEARCH-FN.
This setting is used internally by the PRESS-DOWN command.

TPS documentation homepage


PRESS-DOWN : TESTCMD

PRESS-DOWN is a test-top command.
Before using this command, use the MODE command to
set up a mode in which the current theorem can be proven. Also
check the value of the TEST-INITIAL-TIME-LIMIT flag (it should
be high enough that the first attempt at proof will succeed).
Then PRESS-DOWN will systematically vary the values of the flags
listed in the TEST-FASTER-IF-* flags, using the PRESS-DOWN search
function (see the help message for TEST-NEXT-SEARCH-FN).
The values of TEST-REDUCE-TIME, TEST-NEXT-SEARCH-FN and
TEST-FIX-UNIF-DEPTHS will be permanently changed (to T, PRESS-DOWN
and T respectively).

Note that this is NOT the same as PRESS-DOWN-2, since it automatically
generates a searchlist rather than relying on the user to provide one.
 
The command format for PRESS-DOWN is:

<TEST>PRESS-DOWN MODENAME TESTWIN
"SYMBOL" "YESNO"

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage