ECONJ-TAC : TACTICECONJ-TAC is a tactic.
As defined for use NAT-DED: is a primitive tactic.
Applies ECONJ if a support line is a conjunction.
As defined for use ETREE-NAT: is a primitive tactic.
Applies conjunction elimination to a support line if applicable.
Pfenning's tactics 199-200, but regardless of whether the conjuncts
are both essential to proving the planned line.
TPS documentation homepage