PROP-PRIM : TACTIC

PROP-PRIM is a tactic.
As defined for use NAT-DED:
(ORELSE SAME-TAC TRUTH-TAC ABSURD-TAC INDIRECT2-TAC MAKE-ROOM ECONJ-TAC
ICONJ-TAC EQUIV-IMPLICS-TAC IMPLICS-EQUIV-TAC PUSHNEG-TAC PULLNEG-TAC
DEDUCT-TAC MP-TAC CASES-TAC INDIRECT-TAC)
Much like tactic defined in Felty's master's thesis, p. 64.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage