GO2-TAC : TACTIC

GO2-TAC is a tactic.
As defined for use NAT-DED:
(REPEAT
(ORELSE (CALL PRINT-ROUTINES) SAME-TAC REFL=-TAC SYM=-TAC RULEP-TAC
PROP-INTRO-RULES-TAC PROP-ELIM-RULES-TAC PUSHNEG-TAC UGEN-TAC
RULEC-TAC SUB=-TAC PULLNEG-TAC INDIRECT-EXISTS-PLINE-TAC
INDIRECT-DISJ-PLINE-TAC EQUIV-EQ-CONTR-TAC EQUIV-EQ-EXPD-TAC EXT=-TAC
EXT=0-TAC ELIM-DEFNS-TAC LEXPD*-VARY-TAC LCONTR*-VARY-TAC))

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage