MONSTRO-TAC : TACTIC

MONSTRO-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 UI-HERBRAND-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