INEG-TAC : TACTIC
INEG-TAC
is a tactic.
As defined for use
NAT-DED
: is a primitive tactic.
Applies
INEG
if the planned
line
is a negated formula.
As defined for use
ETREE-NAT
: is a primitive tactic.
Applies
INEG
if planned
line
is a
negation
.
TPS documentation homepage
© 1988-99, Carnegie Mellon University.
TPS homepage