COMPLETE-TRANSFORM*-TAC : TACTIC

COMPLETE-TRANSFORM*-TAC is a tactic.
As defined for use ETREE-NAT:
(ORELSE (CALL PRINT-ROUTINES) SAME-TAC ABSURD-TAC TRUTH-TAC REFL=-TAC
(IFTHEN USE-RULEP-TAC RULEP-TAC) (MAKE-ROOM :USE NAT-DED)
(THEN** (IFTHEN USE-RULEP-TAC ECONJ*-TAC ECONJ-TAC) UNSPONSOR-TAC)
DEDUCT-TAC REWRITE-SLINE-TAC REWRITE-PLINE-TAC RULEC-TAC UGEN-TAC
EGEN-TAC (THEN** UI-TAC UNSPONSOR-TAC)
(THEN** UNNEC-EXP-TAC UNSPONSOR-TAC) (THEN** IDISJ-TAC UNSPONSOR-TAC)
(THEN** (IFTHEN USE-RULEP-TAC ICONJ*-TAC ICONJ-TAC) UNSPONSOR-TAC)
(THEN** CASES-TAC UNSPONSOR-TAC) PUSHNEG-TAC NEG-NEG-PLAN-TAC INEG-TAC
SUBST=-TAC MP-TAC CLASS-DISJ-TAC INDIRECT2-TAC INESS-PLINE-TAC
NEG-AND-SLINE-TAC NEG-AND-PLAN-TAC NEG-EQUAL-SLINE-TAC INDIRECT-TAC)

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage