DIY-TAC is a tactic.
As defined for use NAT-DED: is a primitive tactic.
Calls matingsearch procedure specified by the flag DEFAULT-MS on current
planned line and its supports, then translates the expansion proof to
natural deduction. The actual supports used will be the universal closure
of the supports over any free variables which are not free in their

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage