USE-DIY : FLAG

USE-DIY is a flag or parameter.
When T, proof lines which are proven by DIY, DIY-L or UNIFORM-SEARCH-L
will not be translated into natural deduction style, but will instead be
justified in a single step, as "Automatic" from the support lines.
A comment will be added to the relevant line of the proof showing the
time taken and the mode used for the automatic proof.

Obviously, ND proofs containing justifications of this sort cannot be translated by
NAT-ETREE.
USE-DIY takes values of type BOOLEAN.
It belongs to subjects OTL-VARS TACTICS MATING-SEARCH ETR-NAT .
Its default value is NIL
Its current value is NIL.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage