SUBST=-BACKCHAIN-LEMMA-TAC : TACTIC

SUBST=-BACKCHAIN-LEMMA-TAC is a tactic.
As defined for use ETREE-NAT: is a primitive tactic.
If substitution of equality can be applied to a support line, creates
a new disjunctive lemma based on the formula to which the equality can
be applied. Then symmetric simplification is used to simplify the lemma.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage