PLINE-TAC : TACTIC

PLINE-TAC is a tactic.
As defined for use ETREE-NAT:
(ORELSE DEDUCT-TAC ICONJ-TAC IDISJ-RIGHT-TAC IDISJ-LEFT-TAC
IMPLICS-EQUIV-TAC LEXPD*-VARY-TAC AB-PLAN-TAC EQUIV-WFFS-PLAN-TAC
EQUALITY-PLAN-TAC RULEQ-PLAN-TAC UGEN-TAC EGEN-TAC TRUTH-TAC)

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage