NEG-EQUAL-SLINE-TAC : TACTIC
NEG-EQUAL-SLINE-TAC
is a tactic.
As defined for use
ETREE-NAT
: is a primitive tactic.
If a support
line
is a negated equality and planned
line
is
falsehood
,
applies
indirect
proof. Similar to Pfenning's tactic 217.
TPS documentation homepage
© 1988-99, Carnegie Mellon University.
TPS homepage