DIY-TAC : TACTIC

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
hypotheses.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage