As defined for use NAT-DED: is a primitive tactic.

Applies PULLNEG if the planned line is a negated non-literal formula.

If planned line is a negated formula, calls the appropriate tactic

for pulling the negation out.

As defined for use ETREE-NAT:

(IFTHEN (NEG-PLINE-P-TAC)

(ORELSE NEG-NEG-PLAN-TAC NEG-OR-PLAN-TAC NEG-IMP-PLAN-TAC

NEG-SEL-PLAN-TAC NEG-EXP-PLAN-TAC NEG-REW-PLAN-TAC))

If planned line is a negated formula, calls the appropriate tactic

for pulling the negation out.

© 1988-99, Carnegie Mellon University.