REWRITE-PLINE-TAC : TACTIC

REWRITE-PLINE-TAC is a tactic.
As defined for use ETREE-NAT:
(IFTHEN (REWRITE-PLINE-P-TAC)
(ORELSE AB-PLAN-TAC EQUALITY-PLAN-TAC EQUIV-WFFS-PLAN-TAC
RULEQ-PLAN-TAC LEXPD*-VARY-TAC IMPLICS-EQUIV-TAC
ML::TRUTHP-REWRITE-PLAN-TAC))
If the planned line corresponds to a rewrite node, calls the appropriate
tactic.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage